автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.18, диссертация на тему:Символьная верификация непрерывно-дискретных систем. Алгоритм обобщенного таймер-преобразования

На правах рукописи УДК 681.142.21

ОД

? я пс1

Парийская Екатерина Юрьевна

СИМВОЛЬНАЯ ВЕРИФИКАЦИЯ НЕПРЕРЫВНО-ДИСКРЕТНЫХ СИСТЕМ.

АЛГОРИТМ ОБОБЩЕННОГО ТАЙМЕР-ПРЕОБРАЗОВАНИЯ

05.13.18. — теоретические основы математического моделирования, численные методы и комплексы программ

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

/

САНКТ-ПЕТЕРБУРГ 2000

Работа выполнена в Санкт-Петербургском государственном техническом университете

Научные руководители:

доктор техн. наук, профессор Карпов Ю. Г. Санкт-Петербургский государственный технический университет

кандидат физ.-мат. наук, доцент Сениченков Ю. Б. Санкт-Петербургский государственный технический университет

Официальные оппоненты:

доктор физ.-мат. наук, профессор Осипенко Г. С. Санкт-Петербургский государственный технический университет

кандидат физ.-мат. наук, ст.н.с. Васильев Н. Н. Петербургское отделение математического института им. В.А.Стеклова РАН

Ведущая организация:

Санкт-Петербургский институт информатики и автоматизации РАН

Защита диссертации состоится 30 мая 2000 г. в 16 часов на заседании диссертационного совета К 063.38.30 Санкт-Петербургского государственного технического университета по адресу: 195220, г. Санкт-Петербург, Гражданский пр., д.28

С диссертацией можно ознакомиться в библиотеке СПбГТУ по адресу, г. Санкт-Петербург, ул.Политехническая, 29

Автореферат разослан « » апреля 2000 г.

Учёный секретарь диссертационного совр™

доктор техн. наук

Арсеньев Д.Г.

Общая характеристика работы

Актуальность работы. Сложность управляемых систем постоян-ю увеличивается вследствие научно-технического прогресса. Возни-сают новые проблемы, связанные с параллельностью, раснределен-гастыо, иерархией в сложных системах, повышаются требования к »ффективности, безопасности и надежности систем автоматического вправления. В результате интенсивного использования электронно-вычислительной техники в системах управления на современной стадии сомпыотеризации общества появилась необходимость проектирования и шализа так называемых "непрерывно-дискретных" (или "событийно-шравляемых") систем, математические модели которых объединяют > себе как нетривиальные непрерывные поведения, так и нетривиальнее дискретные поведения. На протяжении уже сорока лет разными шторами (А.А.Андронов, Ю.И.Неймарк, Н.П.Бусленко, В.М.Глушков, З.С.Емельянов и др.) велись разработки в области качественного ана,-шза и моделирования непрерывно-дискретных систем. Анализ математических моделей и методов, которые лежат в основе современных ¡ычислительных комплексов, показывает, что сегодня применяются два >сновных подхода к моделированию непрерывно-дискретных систем — федставление поведения системы в виде последовательности классиче-:ких динамических систем и численное "траекторное" моделирование гли упрощение непрерывной части и использование технологии дискрет-юго моделирования и анализа. Между тем, специфика непрерывно-диск->етной системы заключается в нетривиальности каждой из ее компонент (как непрерывной, так и дискретной) и упрощение поведения той 1ли иной компоненты приводит к неполноте ее математической модели I проводимого анализа. Применение численного моделирования предста-щяется чрезвычайно трудоемкой задачей при анализе свойств поведения гепрерывпо-дискретных систем. Кроме того, в непрерывно-дискретных :истемах возникают проблемы, типичные для параллельных и распреде-шнных систем, которые можно эффективно решить методами верификации дискретных параллельных систем (вопросы взаимодействия параллельных компонент, проблемы тупиков и зацикливаний, проблемы >азработки синхронизирующих примитивов, защиты ресурсов). В нача-хе 90-х годов возник новый гибридный (или символьный) подход, базирующийся на методах дискретного темпорального подхода, развитого в работах Ч.Хоара, Б.Кларка, Е.Эмерсона, А.Пнуэли и других современных авторов для решения задач моделирования и анализа дискретных

параллельных и распределенных систем. Привлекательность гибридного подхода до сравнению с численным моделированием заключается в возможности анализа качественных свойств поведения и оценок областей достижимости системы без траекторного моделирования, в возможности исследования вопросов взаимодействия параллельных компонент в непрерывно-дискретных системах, в возможности интервального задания параметров и проведения интервального параметрического анализа, наконец, в неограниченной сложности дискретной компоненты в исследуемых системах. Гибридный подход представляется актуальным современным направлением моделирования и анализа непрерывно-дискретных систем. Развитие символьных методов верификации и внедрение их в современные вычислительные комплексы позволит значительно расширить возможности моделирования и анализа свойств поведения непрерывно-дискретных систем.

Цель работы. Целью работы является создание новых средств моделирования и качественного анализа непрерывно-дискретных систем. В частности в работе решались следующие задачи:

1. Анализ гибридного направления моделирования и качественного анализа непрерывно-дискретных систем; исследование границ разрешимости символьных методов верификации.

2. Распространение символьных методов верификации дискретных систем реального времени на более широкий класс непрерывно-дискретных систем.

Методы исследования. В работе использованы математическая теория систем, методы качественного анализа динамических систем, теории ОДУ, интервального анализа, методы теории гибридных систем, темпоральная логика и теория автоматов. Научная новизна работы.

1. Для класса гибридных автоматов с линейными системами дифференциальных уравнении с постоянными коэффициентами и ограниченной интервальной инициализацией разработан алгоритм линейной аппроксимации "обобщенное таймер-преобразование". Алгоритм позволяет распространить применение символьных методов верификации на более широкий класс непрерывно-дискретных систем. Расширение класса достигнуто благодаря обогащению гибридного подхода методами численного и интервального анализа.

2. Сформулированы и теоретически обоснованы условия применимости алгоритма обобщенного гаймер-цреобразования для гибридного автомата с линейными системами дифференциальных уравнений с постоянными коэффициентами и ограниченной интервальной инициализацией.

3. Доказана теорема о сходимости метода символьной верификации для линейной аппроксимации гибридного автомата с линейными системами дифференциальных уравнений, построенной с помощью обобщенного таймер-преобразования.

4. Доказана теорема о сходимости метода символьной верификации для линейной аппроксимации параллельной композиции гибридных автоматов с линейными системами дифференциальных уравнений, построенной с помощью обобщенного таймер-преобразования.

5. Доказана теорема о корректности положительных результатов символьной верификации для гибридных автоматов с линейными системами дифференциальных уравнений и их параллельной композиции. Практическая ценность и реализация результатов. Алгоритм обобщенного таймер-преобразования позволяет расширить возможности различных существующих систем компьютерного моделирования. В настоящее время начата реализация алгоритма обобщенного таймер-преобразования в системе компьютерного моделирования Model Vision 3.0. В процессе работы подтвердилось предположение о том, что метод символьной верификации совместно с алгоритмом обобщенного таймер-преобразования в численных компьютерных системах моделирования может значительно упростить процесс моделирования непрерывно-дискретных систем, так как в этом случае становится возможным проверка качественных свойств поведения системы и параметрический интервальный анализ на предварительном этапе моделирования, а также позволит исследовать вопросы параллелизма и взаимодействия компонент непрерывно-дискретной системы. В компьютерных системах дискретного моделирования (Covers ж др.) реализация алгоритма позволит проводить качественный анализ поведения непрерывно-дискретных систем чисто дискретными методами, если выполнены условия приводимости анализируемой системы к системе временных переходов. В компьютерных системах моделирования, основанных на символьной верификации, (HyTech и др.) реализация алгоритма значительно расширит класс непрерывно-дискретных систем, для которых возможна верификация. В процессе разработки алгоритма предложен метод покоординатных оце-

нок для задачи оценивания фазового состояния линейной системы ОДУ. Реализация этой части алгоритма в компьютерных системах моделирования позволит задавать начальные условия в виде интервалов при моделировании и анализе непрерывно-дискретных систем с линейными системами ОДУ.

Основные положения, выносимые на защиту:

• алгоритм линейной аппроксимации для гибридных автоматов с системами дифференциальных уравнений с постоянными коэффициентами и ограниченной интервальной инициализацией;

• формулировка и теоретическое обоснование условий применимости разработанного алгоритма для класса непрерывно-дискретных систем, описываемых моделью гибридного автомата с системами дифференциальных уравнений с постоянными коэффициентами и ограниченной интервальной инициализацией и их параллельной композиции;

• доказательство сходимости метода символьной верификации для линейной аппроксимации гибридного автомата с линейными системами дифференциальных уравнений, построенной с помощью обобщенного таймер-преобразования; доказательство сходимости метода символьной верификации для линейной аппроксимации параллельной композиции гибридных автоматов с линейными системами дифференциальных уравнений, построенной с помощью обобщенного таймер-преобразования;

• доказательство утверждения о том, что для линеаризованного автомата положительные результаты верификации и только они являются корректными, являющегося обоснованием возможности совместного использования разработанного алгоритма и метода символьной верификации в задачах моделирования и качественного анализа непрерывно-дискретных систем.

Апробация работы. Основные результаты работы докладывались и обсуждались на международных и всесоюзных научно-технических семинарах и конференциях: ежегодная научно-техническая конференция "Фундаментальные исследования в технических университетах" (СПбГТУ,1997,1998,1999гг.), вторая международная научно-техническая конференция "Дифференциальные уравнения и приложения" (СПбГТУ, 1998г.), а также на семинарах в С.-Петербургском институте ин-

форматики и автоматизации РАН (1999г.), в институте теоретической астрономии РАН (1998г.), в Ярославском государственном университете (1999г.) и на кафедрах СПбГТУ (1995, 1996, 1997, 1999гг.). Публикации. По результатам исследования опубликовано 8 работ. Личный вклад автора. Все результаты работы, выносимые на защиту, получены лично автором.

Структура и объем работы. Диссертационная работа состоит из введения, двух глав, заключения и двух, приложений. Объем основного текста составляет 130 страниц, иллюстрированных 8 рисунками, приложения занимают 22 страницы. Список литературы составляет 76 наименований.

Содержание работы

Во введении обоснована актуальность работы, формулируются цели и задачи работы. Вводится понятие непрерывно-дискретной системы, рассматривается специфика поведения и основные свойства систем этого класса.

Первая глава содержит необходимые сведения о дискретном темпоральном подходе, развитом в работах Ч.Хоара, Л.Лэмпорта, Е.Кларка, Е.Эмерсопа, А.Пнуэли, Д.Харела, З.Манны и других современных авторов для решения задач моделирования и анализа дискретных параллельных и распределенных систем, и о гибридном направлении исследования непрерывно-дискретных систем. Представлены базовые математические модели дискретного темпорального подхода (система переходов, система временных переходов и таймированный автомат), которые лежат в основе гибридного направления. Определены понятия гибридного автомата, параллельной композиции гибридных автоматов, рассмотрены отдельные классы гибридных автоматов (линейный гибридный автомат, линейный гибридный автомат с постоянными коэффициентами, прямоугольный автомат). Представлены основные классификации требований к поведению параллельных систем, которые могут быть верифицированы в рамках дискретного темпорального подхода (классификация Л.Лэмпорта, Борелл-классификация), и базовый язык спецификаций требований к поведению (темпоральная логика).

Далее подробно рассмотрен метод символьной верификации гибридных автоматов, приведены примеры верификации систем автоматического управления. Представлен краткий обзор материалов по исследованию условий сходимости метода символьной верификации гибридных автоматов. Показано, что максимальным классом разрешимости символь-

ного метода является прямоугольный автомат с ограниченной интервальной инициализацией. Представлены существующие алгоритмы линейной аппроксимации гибридных автоматов — таймер-преобразование (II.Xo, 1994г.) и 6 -amiр оксимаци я но производной (П.Хо, Т.Хензингер, 1995г.), обсуждаются их недостатки, демонстрируются примеры линейной аппроксимации. Результаты анализа гибридного направления могут быть сформулированы в следующих пунктах:

• привлекательность символьного подхода к моделированию и анализу свойств поведения непрерывно-дискретных систем по сравнению с численным моделированием заключается:

- в возможности анализа качественных свойств поведения и оценок областей достижимости системы без траекторного моделирования;

- в возможности исследования вопросов взаимодействия параллельных компонент в непрерывно-дискретных системах;

- в неограниченной сложности дискретной компоненты;

- в возможности задания параметров в виде интервалов и параметрического анализа;

• гибридное направление сегодня не может конкурировать с современными численными компьютерными системами моделирования, так как максимальным классом разрешимости символьных методов является прямоугольный автомат;

• один из возможных путей распространения символьного анализа на более широкие классы непрерывно-дискретных систем заключается в значительном расширении набора алгоритмов линейной аппроксимации гибридных автоматов.

Во второй главе представлен разработанный автором новый алгоритм линейной аппроксимации гибридных автоматов. В основу алгоритма положена схема, предложенная П.Хо в алгоритме таймер-преобразования для линеаризации одной переменной гибридного автомата, локальные поведения которой описываются дифференциальными уравнениями вида х — f(x). Новый алгоритм является обобщением таймер-преобразования на случай п переменных, локальные поведения которых описываются системами линейных дифференциальных уравнений.

Введем новый класс гибридных автоматов с линейными системами дифференциальных уравнений.

Определение 1 Гибридным автоматом с линейными системами дифференциальных уравнений называется гибридный автомат: Ноду = { Ц V, X, Е, flow, pre, post, inv, init, syn }, где

2 — конечный входной алфавит (алфавит событий); V — конечное множество вершин автомата (локаций); X — конечное, множество фазовых переменных (будем представлять его в виде вектора х — [xi,..я„], х,- £ X); Е — конечное множество дуг; syn : Е —* Е - заданное конечное отображение;

flow — конечное множество локальных поведений фазовых переменных вида:

flow(v, х) : ^ = Avx + Ь„ где Av - матрица линейной системы ОДУ с постоянными коэффициентами в локации v, Ьц - вектор постоянных коэффициентов неоднородной системы ОДУ в локации v, a,j, bi £ R;

pre - конечный набор логических формул над множеством фазовых переменных вида:

рге(е) : А,- р,-

где pi ~ E"=i hjxj ~ с - термы, hj, с £ R, {<, <, =,>,>}, е £ Е;

post - набор мгновенных действий (инициализаций) при смене локальных поведений вида:

post(e) : {z; := Cj, г £ 1.. .тг}, с,- £ [fj ;«,•], 1{,щ £ R, е £ Е; inv — конечное множество логических формул (предикатов-инвариантов ), описывающих дополнительные ограничения на значения фазовых переменных в локациях вида:

inv(v) : Ai Pi

где pi = J2"=i hjXj ~ с - термы, hj, с 6 R, {<, <, =, >, >}, v £ V;

init - предикат, описывающий множество начальных локаций и области начальных значений фазовых переменных: init(v) : {zi'.— Ci, г=1...га} V False, с,- £ [i,-; u,], U, щ £ R, v £ V"; Каждая дуга e £ E помечена буквой алфавита событий а = syn(e), условием перехода по дуге рге(е) и формулой преобразования фазовых переменных на дуге post(e).

Пусть Т - множество всевозможных ограниченных вещественных интервалов, V - множество всевозможных ограниченных прямоугольных областей (прямоугольных параллелепипедов) в R".

Назовем дугу е, входящую в локацию v гибридного автомата, "синхронизированным входом" локации v, если множество мгновенных действий на ней имеет вид: post(e) : {аг,- := с,-, г = 1.. .гг}, с,- £ /,■ £ Т. Множество входных значений {х^} локации v является прямоугольным параллелепипедом в Rn, {х^} = D £ V. Назовем дугу е, выхо-

дящую из локации V гибридного автомата, "синхронизированным выходом" локации V, если условие перехода на ней имеет вид: рге(е) : Л-'=1 а,- < я,- < 6,-, [а,-,Ь,] £ Т. Множество значений {х-"-1}, соответствующее переходу из локации и по дуге е является прямоугольным параллелепипедом в Л", {х^^} = В € V. Произвольный цикл гибридного автомата будем называть "синхронизированным", если хотя бы одна локация, участвующая в нем, имеет синхронизированный вход или синхронизированный выход. Для несинхронизированных циклов гибридного автомата определим свойство "неразрастания" фазовых траекторий. Будем говорить, что при обходе несинхронизированного цикла пучок фазовых траекторий не разрастается, если для каждой локации V, участвующей в цикле, множество входных значений {х^} обладает

СВОЙСТВОМ {х^} после обхода С {х^}до обхода- БуДеМ ГОВОриТЬ, ЧТО ГИбрИДный автомат с линейными системами ОДУ обладает свойством ограниченной интервальной инициализации, если: 1) предикат гпИ описывает все области начальных значений в виде ограниченных прямоугольных областей; 2) для каждой дуги автомата е множество розЬ(е) имеет вид: {дг,- := с,-, г е 1.. .п}, с,- € Г,-, Г, е 1-

Пусть дан гибридный автомат с линейными системами дифференциальных уравнений Н. Пусть автомат Н обладает свойством ограниченной интервальной инициализации и все его несинхронизированные циклы обладают свойством неразрастания фазовых траекторий. Поставим задачу его символьной верификации. Будем решать ее следующим образом: построим линейную аппроксимацию гибридного автомата; модифицируем требования к поведению для построенной модели поведения; верифицируем построенную модель методом символьной верификации.

Для построения линейной аппроксимации предлагается алгоритм обобщенного таймер-преобразования. На вход алгоритма обобщенного таймер-преобразования подается гибридный автомат П с линейными системами ОДУ. С помощью алгоритма строится автомат Т#, который является линейной аппроксимацией исходного автомата. Алгоритм обобщенного таймер-преобразования; Шаг 1. Для произвольной локации V гибридного автомата Н вычисляем аппроксимации всех множеств возможных входных значений вектора фазовых переменных. Для этого будем идти по всем путям, ведущим в локацию V, до первого синхронизированного входа или синхронизированного выхода (либо мы дойдем до начальной локации автомата, либо до локации, участвующей в цикле, проходящем через V, с известными

входными шш выходными значениями всех компонент вектора фазовых переменных, либо вернемся в исходную локацию по несянхронизирован-ному циклу, в последнем случае помечаем цикл) и отслеживать развитие х (пучка траекторий) вплоть до локации V путем последовательного решения задач оценивания фазового состояния линейпых систем ОДУ с прямоугольными областями начальных значений.

Шаг2. Разбиваем локацию V на подлокации ..., V*.} (к - число различных множеств входных значений х в локации V, в худшем случае к = со + с„, где со - количество начальных локаций автомата, сг, - количество циклов, проходящих через и), каждая из которых имеет свою область входных значений Хд1'^ ~ ХИ"1^ £ Р. Каждая новая подлокация v¡ соединяется дугами со всеми такими локациями г/, что в исходном автомате существовали дуги и') , и с одной локацией у", такой что в исходном автомате существовала дуга е(ь",г\) и именно по вей шло вычисление входного значения Хд подлокации (с наследованием предикатов рге(е) и розЦе)). Следует объединить подлокации с одинаковыми областями входных значений и удалить подлокации, в которых начальные значения не удовлетворяют инварианту х^ ^

Повторяем шаг 1 и шаг 2 последовательно для всех локаций автомата. Шаг 3. Вектор фазовых переменных заменяем на (единственный) таймер ¿X; который запускается во всех подлокациях (предикаты роа^е) заменяются на 1х '.= 0). Предикаты рге(е) на выходящих дугах из локации V и предикаты-инварианты ту(ь) заменяются на ограничения по длительности нахождения в локации и,- вида < £ < , где значения берутся из решений задач оценивания фазового состояния для подлокации и; и условия перехода по дуге рге(е).О

Свойство неразрастания несинхронизированных циклов проверяется по ходу выполнения шага 1 алгоритма исследованием каждого из всех вычисленных множеств возможных входных значений локации V на неразрастание при обходе помеченных циклов путем последовательного решения задач оценивания фазового состояния для локаций, участвующих в циклах.

Вычислительная сложность алгоритма равна вычислительной сложности решенияр-(со+с„) задач оценивания фазового состояния линейной системы ОДУ (р - число локаций автомата, со - число входных локаций, с„ - число циклов, в которых участвуют локации). Построенная линейная аппроксимация имеет р ■ к(у) локаций (к(ю) - число различных областей начальных значений вектора переменных в локациях). Для ре-

шсния задач оценивания предлагается метод покоординатных оценок, который дает аппроксимацию множества, достижимости системы, соответствующего истинности предиката в отдельно взятой локашш, классом прямоугольных параллелепипедов в Л" и оценки соответствующего этому множеству временного интервала. Для оценивания временного интервала отдельно предлагается метод оценки временного интервала.

Пусть Н - гибридный автомат с линейными системами ОДУ, Тц -линейная аппроксимация гибридного автомата Н, построенная с помощью обобщенного таймер-преобразования. В работе доказаны следующие утверждения:

Теорема 1 Автомат Тц, построенный для гибридного автомата Н с помощью обобщенного таймер-преобразования, является системой временных переходов.

Теорема 2 АвтоматТц допускает все пробеги, допустимые в исходном автомате Н. Обратное утверждение неверно:

Неаск(Н) С Яеаск(Ти).

(Не,асЬ,(Н) - глобальное множество достижимых состояний гибридного автомата Н).

Из теорем 1 и 2 следует, что метод символьной верификации можно использовать для верификации тех свойств поведения гибридного автомата с линейными системами ОДУ, результат верификации которых на линейной аппроксимации автомата положителен.

Пусть теперь дана параллельная композиция из т гибридных автоматов, часть из которых является гибридными автоматами с линейными системами ОДУ, а часть принадлежит к классам гибридных автоматов, для которых доказана сходимость метода символьной верификации. Предположим также, что множества фазовых переменных гибридных автоматов не пересекаются, но Е,-Г)Еу ф 0, где Е,- - алфавит событий автомата г. Применим алгоритм обобщенного таймер-преобразования последовательно для всех гибридных автоматов с линейными системами ОДУ и заменим гибридные автоматы Щ с линейными системами ОДУ их линейными аппроксимациями Т{. Получим параллельную композицию Ь автоматов 3*, Нк+1, • • •, Нт. В работе доказаны следующие утверждения о линейной аппроксимации параллельной композиции гибридных автоматов с линейными системами ОДУ:

Теорема 3 Пусть £ - параллельная композиция автоматов Н\,..., Щ, Т)с+1,...,Тт, в которой Н\,...Нк - гибридные автоматы с линейными системами ОДУ, 1,..., Тт - таймированные автоматы. Пусть мно-

жества фазовых переменных гибридных автоматов В],.. .IIк не пересекаются: V«',1 < г < к, I <] < т,ХщГ\Хат = 0, Хц,Г\Хг^ = 0. Тогда автомат Тпостроенный с помощью обобщенного таймер-преобразования для параллельной композиции автоматов Ь, является тай-мированпым автоматом.

Теорема 4 Пусть Ь - параллельная композиция автоматов Н\,..., //<-, Нк+1,.. - ,Нт, в которой Щ,.. .Нк - гибридные автоматы с линейными системами ОДУ, ifjt.fi,..., Нт - прямоугольные автоматы с ограниченной интервальной инициализацией. Пусть множества фазовых переменных гибридных автоматов Н\,... II^ не пересекаются; У г, ]. 1 < г < к, 1 < з < т, Xя.: П Хгг= 0. Тогда автомат Ть, построечный с помощью обобщенного таймер-преобразования для параллельной композиции автоматов Ь, является прямоугольным автоматом с ограниченной интервальной инициализацией.

Теорема 5 Пусть Ь - параллельная композиция автоматов ..., IIь, Нк+г, ■. ■, Нт> в которой Иг,... Ли - гибридные автоматы с линейными системами ОДУ, Нь+х,. ■ .,Нт - линейные гибридные автоматы с постоянными коэффициентами. Пусть множества фазовых переменных гибридных автоматов Н\,...Нк не пересекаются: Vi,j1 1 < г < к, 1 < ] < т, Хц{ П Хп„, — 0- Тогда автомат Тс, построенный с помощью обобщенного таймер-преобразования для параллельной композиции автоматов Ь, является линейным гибридным автоматом с постоянными коэффициентами.

Из теорем 2, 3, 4, 5 следует, что метод символьной верификации можно использовать для верификации тех свойств поведения параллельной композиции гибридных автоматов с линейными системами ОДУ, результат верификации которых на линейной аппроксимации параллельной композиции положителен.

В работе формулируются и обосновываются условия применимости обобщенного таймер-преобразования к гибридному автомату с линейными системами ОДУ.

Теорема 6 Обобщенное таймер-преобразование применимо к гибридному автомату с линейными системами дифференциальных уравнений, если количество возможных интервально заданных начальных значений вектора переменных в каждой локации автомата конечно. Теорема 7 Количество возможных интервально заданных начальных значений вектора переменных х в локации V гибридного автомата с линейными системами ОДУ конечно, если

1) в предикате iriit автомата имеется инициализация всех переменных в виде ограниченных интервалов;

2) каждый цикл в автомате, проходящий через локацию v,

в либо является синхронизированным, то есть можно найти дугу е, для которой выполнено одно из следующих условий:

— имеется инициализация всех переменных одновременно в виде ограниченных интервалов ("синхронизированный вход")

post(e) : {ж,- := с„ г = 1... тг}, с,- € [h, и,-], [/,-, «,•] € 1]

— условие перехода по дуге содержит ограничения на все переменные одновременно в виде ограниченных интервалов ("синхронизированный выход")

pre{e) : A?=1 /,■ <х{< щ, в X;

• либо обладает свойством неразрастания фазовых переменных, то есть при обходе цикла все возможные области начальных значений jxo(w)} вершины v не расширяются:

V{xoO)} : {x0(u)}noc;ie обхода Q {Хо(и)}до обхода Теорема 8 Обобщенное таймер-преобразование применимо к гибридному автомату с линейными системами дифференциальных уравнений, если он обладает свойством ограниченной интервальной инициализации и если в процессе построения не нарушается свойство ограниченности областей входных значений каждой локации автомата. Метод покоординатных оценок. Пусть дана линейная система дифференциальных уравнений с постоянными коэффициентами размерности п : dx/dt = Ах + b, ntj, bi 6 R] область начальных значений задана в виде прямоугольного параллелепипеда в Rn: Д) = {/; < х^ < = 1... n, [/,-, it;] 6 I}. Требуется: 1) вычислить интервал времени [th i2], когда пучок решений задачи Коши x(i) в первый раз будет удовлетворять предикату Р : S"=1/t;:r,- ~ с, hi, с € {<,<,=,>,>} (будет нахо-

диться в области фазового пространства системы, ограниченной неравенством S"=1/ijXi ~ с). 2) оценить множество значений вектора х (прямоугольным параллелепипедом в R"), соответствующее первому пересечению пучка решений задачи Коши х(<) и области фазового пространства системы, ограниченной предикатом Р.

Доказывается утверждение о том, что в каждый фиксированный момент времени множество достижимости линейной системы ОДУ с постоянными коэффициентами и множеством начальных значений, заданных прямоугольным параллелепипедом в R", представляет собой (косоугольный) параллелепипед в R". На основании этого утверждения метод сводится

к последовательному решению задач Копти ^ = Ах -f- b, х(0) = xq, в которых xq являются вершинами исходного прямоугольного параллелепипеда Д), к вычислению экстремальных значений решений задач Коти в области, ограниченной предикатом Р (и соответствующих интервалов [ii,^]), и к выбору из полученного множества экстремальных значений минимального и максимального xmin, хтаг, а из множества интервалов самого широкого интервала [imin,tmax\- Если после перебора всех вершин окажется, что xmi-„ = хтаг — 0, то это значит, что пучок решений задачи Коши никогда не окажется в заданном полупространстве. В обобщенном таймер-преобразовании дуга, помеченная предикатом Р, должна быть удалена (предикат на дуге заменен на False). Если после перебора всех вершин окажется, что im,-„ = 0, tmax = со то это значит, что пучок решений задачи Коши всегда будет находиться в заданном полупространстве. В обобщенном таймер-преобразовании предикат Р на соответствующей дуге должен быть заменен на True. В остальных случаях получим прямоугольную область D — [xm,n,xm0J,] (возможно неограниченную), И временной Интервал I ~ [tmin,tmax]-

Вычислительная сложность метода покоординатных оценок складывается из вычислительной сложности решения проблемы собственных чисел матрицы размерности п, решения 2" задач отыскания первого неотр.корня вещественной функции и решения п ■ 2" задач на экстремум. Прямоугольный параллелепипед D, построенный методом покоординатных оценок, является верхней оценкой области первого пересечения пучка решений задачи Коши и заданного полупространства, оптимальной в классе прямоугольных параллелепипедов. Интервал времени I, построенный методом покоординатных оценок, описывает точные временные границы, когда пучок решений задачи Коши в первый раз будет находиться в заданном полупространстве.

Метод оценки временного интервала. Пусть дана линейная система дифференциальных уравнений с постоянными коэффициентами размерности п : dx/dt = Лх + Ь, ац, Ь,- G R', область начальных значений задана в виде прямоугольного параллелепипеда в Rn: Do = {/,- < xi0 < Ui,i = 1...П, [i,-, u,-] G J}. Требуется оценить интервал времени [fi, ¿2], когда пучок решений задачи Коши x(t) в первый раз будет удовлетворять предикату Р : Е"=1Л.;Х; ~ с, hi,с £ R,~= {<,<,=,>,>} (будет находиться в области фазового пространства системы, ограниченной неравенством Е"=1/г,а;,' ~ с).

Метод сводится к численному решению полной проблемы собствен-

ных значений матрицы А, вычислению верхней аппроксимации прямоугольным параллелепипедом в Лп области начальных значений в ортогональном базисе и представления предиката в новом базисе в виде функции одной вещественной переменной с интервально-значнымн константами f(t) = ¿с,о), € [¿|, «»],£»(£, ¿¡о) - покомпонентные решения задачи Коши в новом базисе, к = Э — матрица преобразования. Решив задачу интервального анализа о представлении интервально-значной функции f{t) двумя граничными вещественными функциями Ж*)» /гСО в области £ > О, получим два неравенства /] (£) ~ с, /г(£) ~ с. Для вычисления возможных значений при которых пучок решений задачи Коши попадет в нижнее полупространство (исходный предикат £"=1Л,-а:,- < с), достаточно найти первые два нол.корня функции /].(£) — с, для вычисления значений ¿, пучок решений задачи Коши попадет в верхнее полупространство (исходный предикат Е"=1Л,-х,- > с), достаточно найти первые два пол. корня функции /г(^) — с. Если г0,Г1 - найденные корни, то если /1(0) < с (/2(0) > с), то получим ¿ 6 [0; го]; аналогично, если /2(0) > с (/2(0) < с), то t 6 [г0;п]; если /1(0) = с (/2(0) = с), то необходимо более подробное исследование вблизи точки t = 0 (с помощью производных) и выбор одного из предыдущих случаев в зависимости от знака функции (производных) в окрестности нуля.

Вычислительная сложность метода оценки временного интервала складывается из вычислительной сложности решения проблемы собственных чисел матрицы размерности п и отыскания двух первых корней вещественной функции одной переменной. Построенный интервал времени является верхней оценкой искомого временного интервала. В заключении перечислены основные результаты, полученные в работе, и сформулированы некоторые нерешенные вопросы. В приложении 1 анализируется возможность использования символьного подхода для различных математических моделей непрерывно-дискретных систем. В приложении 2 продемонстрирован метод покоординатных оценок на примере динамической модели часовых ходов.

Заключение

Работа посвящена исследованию непрерывно-дискретных систем и разработке новых методов моделирования и качественного анализа для этого класса динамических систем. Основные результаты работы сводятся к следующему:

1. Для класса гибридных автоматов с линейными системами дифференциальных уравнений с постоянными коэффициентами и ограпи-

ченной интервальной инициализацией разработан алгоритм линейной аппроксимации "обобщенное таймер-преобразование". Границы разрешимости метода символьной верификации расширены до подкласса непрерывно-дискретных систем с линейными системами дифференциальных уравнений с постоянными коэффициентами и ограниченной интервальной инициализацией. Расширение класса достигнуто благодаря обогащению гибридного подхода методами численного и интервального анализа. Такт! образом, подтверждена возможность и целесообразность объединения численных и дискретных подходов к анализу непрерывно-дискретных систем.

2. Сформулированы и теоретически обоснованы условия применимости разработанного алгоритма для класса гибридных автоматов с линейными системами дифференциальных уравнений и ограниченной интервальной инициализацией и для их параллельной композиции.

3. Доказаны теоремы о сходимости метода символьной верификации для линейной аппроксимации гибридного автомата с линейными системами дифференциальных уравнений, построенной с помощью обобщенного таймер-преобразования, и для линейной аппроксимации параллельной композиции гибридных автоматов с линейны!,ш системами дифференциальных уравнений.

4. Доказаны теоремы о возможности символьной верификации свойств поведения гибридных автоматов с линейными системами дифференциальных уравнений и ограниченной интервальной инициализацией и их параллельной композиции, результат верификации которых положителен.

Алгоритм обобщенного таймер-преобразования позволяет значительно расширить возможности различных существующих систем компьютерного моделирования. На основании разработанного алгоритма прослеживается путь решения задачи линеаризации для более широкого класса гибридных автоматов (расширение алгоритма обобщенного таймер-преобразования для случая неограниченных интервалов).

Усовершенствованием обобщенного таймер-преобразования может стать добавление в метод покоординатных оценок блока для построения нижних аппроксимаций множества возможных фазовых состояний линейной системы ОДУ. Построение двухсторонних аппроксимаций множеств достижимости линейных систем ОДУ позволит проводить полную верификацию качественных свойств гибридных автоматов описанного класса с помощью алгоритма обобщенного таймер-преобразования и метода символьной верификации.

Публикации по теме диссертации

1. Парийская Е.: Сравнительный анализ математических моделей и подходов к моделированию и анализу непрерывно-дискретных систем. Эл.ж. рег.№ П23275 ''Дифференциальные уравнения и процессы управления", http://www.diff.Alpha.iiep.csa.ru, №1 ,1997, 25с.

2. Парийская Е.: Применение методов теории реактивных систем в задачах моделирования и качественного анализа непрерывно-дискретных систем. Эл.ж. per.Да П23275 "Дифференциальные уравнения и процессы управления", Ш ,1998, 42с.

3. Парийская Е.: Гибридный подход к моделированию и качественному анализу динамических систем. Алгоритмы линейной аппроксимации нелинейного гибридного автомата. Труды 2-ои международной н,-т. конф. "Дифференциальные уравнения и приложения", с.174-177, С.Петербург, 1998г.

4. Парийская Е.: Основные идеи новой технологии моделирования и анализа сложных непрерывно-дискретных систем. Материалы н.-т. конф. "Фундаментальные исследования в технических университетах", с.169-170, С.-Петербург, 1997г.

5. Парийская Е.: Применение гибридного автомата в задачах качественного анализа динамических систем. Материалы н.-т. конф. "Фундаментальные исследования в технических университетах", с. 106-107, С.-Петербург, 1998г.

6. Парийская Е.: Гибридный подход к моделированию и качественному анализу динамических систем. Алгоритм обобщенного таймер-преобразования. Материалы н.-г. конф. "Фундаментальные исследования в технических университетах", с.47-48, С.-Петербург, 1999г.

7. Колесов Ю.Б., Парийская Е.Ю.,Сениченков Ю.Б.: Построение, решение и анализ свойств систем алгебро-дифференциальных уравнений в пакете MODEL VISION 3.0. Вторая международная н.-т. конференция "Дифференциальные уравнения и приложения". Тезисы докладов, с.122-124, С.-Петербург, 1998г.

8. Карпов Ю.Г., Парийская Е.: Качественный анализ гибридных систем. В сб."Вычислительные, измерительные и управляющие системы". Труды СПбПГУ N»449, с. 16-20. С.-Петербург, 1994г.