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

Введение

1 Гибридное направление исследования непрерывно-дискретных систем

1.1 Дискретный темпоральный подход.

1.2 Математические модели дискретного темпорального подхода.

1.3 Классификация и спецификация свойств поведения в дискретном темпоральном подходе, темпоральная логика

1.4 Метод символьной верификации и система HyTech

1.5 Два примера символьной верификации.

1.6 Условия сходимости метода символьной верификации

1.7 Алгоритмы линейной аппроксимации гибридных автоматов

1.7.1 Таймер-преобразование

1.7.2 Алгоритм 6-аппроксимации по производной

1.7.3 Пример: термостат.

1.7.4 Недостатки алгоритмов линейной аппроксимации

2 Алгоритм обобщенного таймер-преобразования для гибридных систем с линейными системами ОДУ с постоянными коэффициентами

2.1 Гибридный автомат с линейными системами ОДУ

2.2 Обобщенное таймер-преобразование.

2.2.1 Схема алгоритма.

2.2.2 Описание алгоритма.

2.3 Теоремы об алгоритме обобщенного таймер-преобразования

2.4 Метод покоординатных оценок. Функция "Cauchy"

2.4.1 Постановка задачи и обоснование решения

2.4.2 Описание метода покоординатных оценок

2.4.3 Функция "extrems" для метода покоординатных оценок.

2.4.4 Теорема о точности метода покоординатных оценок.

2.4.5 Замечание о методе покоординатных оценок . . 114 2.5 Метод оценки временного интервала. Функция "Cauchyl"

2.5.1 Постановка задачи и описание метода.

2.5.2 Теорема о точности метода оценки временного интервала

В настоящее время понятие динамической системы является очень широким, оно охватывает системы любой природы: физической, химической, биологической, технической, производственной, экономической и др. Описание динамических систем также допускает большое разнообразие - от систем дифференциальных уравнений до функций алгебры логики, графов, марковских цепей и т.д. Выбор способа описания зависит от целей исследования и определяет возможные подходы к его исследованию. Современные теории управления и оптимального управления, теория автоматов, алгебраическая теория линейных систем являются различными подходами к исследованию отдельных классов динамических систем. В середине 60-х годов они были впервые объединены в математическую теорию систем.

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

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

В качестве конкретного примера можно привести систему космического слежения, состоящую из нескольких параллельно работающих (и при необходимости заменяющих друг друга) локаторов, каждый из которых является динамической подсистемой. В такой системе управления появление объекта в области видимости некоторого локатора является событием, определяющим его динамику на период слежения. Основным требованием к такой системе управления, очевидно, является надежность работы всей системы при возможных отказах отдельных подсистем и максимальное количество одновременно ведомых объектов. Произвольность траектории ведомого объекта и момента его появления, возможность отказов отдельных элементов делает систему событийно-управляемой и усложняет процесс ее моделирования и анализа. Аналогичным примером может служить система управления наблюдениями на оптических и радиотелескопах сложной структуры, позволяющих наблюдать параллельно несколько небесных объектов и изменяющих программу наблюдений по наступлению разного рода событий (изменения погодных условий, наступления небесных событий, например вспышки сверхновой, отказа записывающих устройств). Специфика подобных систем заключается с одной стороны, в сложности динамики каждого элемента системы (процесс слежения за объектом или наблюдательный эксперимент), а с друw г" ^ гои — в возможности возникновения разного рода событии, которые по-разному в зависимости от момента их наступления мгновенно изменяют динамику элементов и структуру системы в целом.

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

Данная работа посвящена созданию новых методов и алгоритмов моделирования и качественного анализа этого класса динамических систем.

Введем математическую модель непрерывно-дискретной системы и опишем неформально ее основные свойства.

Непрерывно-дискретной системой называется сложная динамическая система, состоящая из большого числа взаимосвязанных и взаи

Дискретный процесс 1

Непрерывное поведение!

Дискретный процесс 2

Непрерывное поведение2 to tl tl системное время

Рис. 1: Схема поведения непрерывно-дискретной системы. модействующих элементов различной природы, а именно из элементов, поведение которых описывается непрерывными процессами, имеющими конечную длительность, и элементов, поведение которых описывается дискретными процессами, время выполнения которых несущественно для анализа системы.

Непрерывно-дискретная система содержит в себе в качестве элементов как объекты динамической природы, являющиеся по сути классическими динамическими системами, так и объекты дискретной природы, являющиеся дискретными системами.

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

Рассмотрим более подробно отдельный элемент системы.

В общем случае поведение элемента может быть представлено тройкой последовательностей:

1. {[^-1, tj), fi(t)}, г = 1,2,. — последовательность локальных поведений, fi - гладкая вещественная функция;

2- ег}, г = 1,2,. — последовательность событий, приводящих к смене локальных поведений;

3. {t{, а;}, г = 1,2,. — последовательность дискретных действий, выполняемых при смене локальных поведений.

Локальные поведения {/,•} образуют множество F допустимых локальных поведений элемента. Значения {ег} "причин смены поведений" образуют множество Е особых событий. Наконец, дискретные действия {аг} образуют множество Act допустимых дискретных действий.

Глобальное поведение элемента — это множество всех возможных поведений при заданных конечных множествах F,E и Act.

Характерными особенностями поведения элемента непрерывно-дискретной системы являются:

• возможность мгновенного изменения значений параметров элемента - разрывы в фазовых траекториях

• возможность мгновенной смены поведения элемента

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

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

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

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

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

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

Таким образом, к основным характеристикам системы в целом следует отнести:

• параллельную композицию элементов как основной принцип конструирования системы

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

• возможность иерархической структуры

• возможность мгновенной смены структуры.

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

Определение (элемент системы). Элементом непрерывно-дискретной системы называется совокупность базовых понятий: Е = { Т , Z , X , Y , F , Е , Act }, где

Т = td : N —» R>о — последовательность временных отсчетов

Z — множество переменных состояний с заданной областью значений D1 х .х Dn

X — множество входных переменных (каналов входа)

У — множество выходных переменных (каналов выхода)

F — множество допустимых локальных поведений

Е — множество причин смены поведения (событий)

Act — множество допустимых дискретных операций

Конкретизация основных компонент элемента порождает различные подклассы непрерывно-дискретных систем. Определение.Непрерывно-дискретной системой называется пара:

S = { Time , Е }, где

Time = R>о — модель времени

Е — модель объекта,являющегося: г) элементом

И) элементом, в котором хотя бы одно локальное поведение заменено на £

Ш) параллельной композицией £ с определенной на ней моделью каналов связей

Разработка методов анализа и моделирования непрерывно-дискретных систем имеет уже более чем сорокалетнюю историю [1, 15, 8, 19, 18, 10, 44]. Вслед за созданием метода точечных преобразований для качественного анализа свойств разрывных колебательных систем в теории нелинейных колебаний (А.А.Андронов, Ю.И.Неймарк и др. [1]), которые можно считать первыми изученными динамическими системами с дискретной компонентой, появляются и различные математические модели и формализмы, предназначенные для моделирования поведения непрерывно-дискретных систем. Среди них агре-гативные системы Н.П.Бусленко (1963г.) [8], непрерывно-дискретная модель В.М.Глушкова (1973г.) [19] и другие.

Среди современных подходов в области моделирования и анализа непрерывно-дискретных систем следует отметить многочисленные попытки создания средств для компьютерного моделирования и автоматического анализа поведения сложных динамических систем с дискретной компонентой в различных пакетах компьютерного моделирования (Simulink [76], TESS [18], VisSim^Statemate MAGNUM1, i-Logic Rhapsody1). Наиболее интересным здесь, как нам кажется, является гибридный подход и модель гибридной системы А.Пнуэли (1992г.) [64].

Информация о системах может быть найдена в международной компьютерной сети InterNet, http://www.vissim.com/vissim.htm

Анализ подходов к моделированию, которые лежат в основе современных вычислительных комплексов, показывает, что сегодня применяются только два подхода к исследованию непрерывно-дискретных систем — представление поведения системы в виде последовательности классических динамических систем и численное "траекторное" моделирование или упрощение непрерывной части и использование технологии дискретного моделирования и анализа. Существующие системы моделирования реализуют, таким образом, лишь ограниченное расширение базовых непрерывных или дискретных моделей и методов.

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

На сегодняшний день подхода, к котором бы одинаково глубоко исследовались оба аспекта непрерывно-дискретной системы, не существует.

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

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

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

Высокий уровень современной технологии моделирования динамических систем (работы в области современной теории управления [21, 17], пакеты Simulink [76], Model Vision 3.0 [57]), появление автоматических методов качественного и параметрического анализа дискретных систем, разработанных в теории реактивных систем (работы Ч.Хоара, Л.Лэмпорта, Е.Кларка, А.Пнуэли, Д.Харела, Т.Хензингера, системы VisSim1, HyTech [51]) предопределяет существование богатой базы для появления такой технологии. Бурное развитие символьного анализа, появление технологии символьных вычислений (пакеты символьных вычислений Mathematica [74], Maple [75]) также оказываются полезными при исследовании сложных и, в частности, непрерывно-дискретных систем.

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

Создание нового подхода к моделированию и качественному анализу непрерывно-дискретных систем, требует, таким образом:

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

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

• выбора необходимых оптимальных методов дискретной и непрерывной области в соответствии с поставленными вопросами

• необходимой модификации, возможного объединения методов для учета влияния компонент друг на друга,

В рамках создания нового подхода к моделированию и качественному анализу непрерывно-дискретных систем автор диссертационного проекта проводит исследования последних достижений в области дискретного моделирования, интересных с точки зрения возможности их включения в такой подход. Основное внимание уделено изучению гибридного направления (современного направления дискретного моделирования непрерывно-дискретных систем) [64, 62, 49, 54, 46], методу символьной верификации [39, 67, 73] и исследованию границ разрешимости гибридных методов [53, 52, 56, 68].

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

Принципиальные моменты гибридного подхода, разработанного как альтернатива численному моделированию, можно сформулировать в следующих пунктах: формализация свойств системы, использование специального языка спецификаций свойств поведения (темпоральная логика), что позволяет формулировать сложные качественные и количественные требования к поведению системы; использование "поведенческих" моделей как средств (графических и текстуальных) компактного и наглядного описания поведения системы, разбиение пространства состояний на классы эквивалентности относительно исследуемых свойств. Это выводит на новый уровень задачу моделирования: вместо многочисленных экспериментов для построения глобального поведения системы достаточно обойти все пути в графе; использование методов автоматической верификации, основанных на достижениях в области символьных вычислений; автоматизация задач качественного параметрического анализа.

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

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

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

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

Алгоритм обобщенного таймер-преобразования позволяет расширить возможности различных существующих систем компьютерного моделирования (система автоматической верификации гибридных систем Ну Tech [51], система дискретного моделирования Covers [7], система моделирования Model Vision [13, 57] и другие). В настоящее время начата реализация алгоритма обобщенного таймер-преобразования в системе компьютерного моделирования Model Vision 3.0.

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

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

Основные результаты работы сводятся к следующему:

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

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

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

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

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

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

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

Благодарности

Автор работы выражает глубокую благодарность своим научным руководителям профессору Ю.Г.Карпову и Ю.Б.Сениченкову за постоянную поддержку и помощь в работе. Автор работы благодарит профессора С.М.Устинова за ценные замечания по опубликованным работам, а также профессора А.А.Первозванского за ценные замечания по работе и консультации в области теории и систем управления, которые повлияли на исследования по теме диссертации. Автор глубоко признателен профессору Ф.Л.Черноусько за консультации по своей книге и ценные советы.

Заключение

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

1. Андронов А.А., Витт А.А., Хайкин С.Э.: Теория колебаний. М: Гос.изд.ф.-м.лит-ры, 1959, 915с.

2. Алефельд Г., Херцбергер Ю.: Введение в интервальные вычисления. Москва, "Мир", 1987, 354с.

3. Арнольд В.И.: Обыкновенные дифференциальные уравнения. Москва, "Наука", 1971, с.240.

4. Баутин Н.Н.: Динамические модели часовых ходов. В сб. "Памяти А.А.Андронова", Изд. АН СССР, 1955.

5. Баутин Н.Н.: Теория точечных преобразований и динамическая теория часов. Труды междун.симп. по нелин. кале б. Изд. АН УССР, Киев, 1963.

6. Беллман Р.: Введение в теорию матриц. Москва, "Наука", 1969, с.368.

7. Борщев А., Карпов Ю., Колесов Ю.: Спецификация и верификация систем логического управления реального времени. В сб. "Системная информатика", вып.2, ИСИ СО РАН, Н-ск, 1993, 40с.

8. Бусленко Н.П.: Моделирование сложных систем. М: "Наука", 1978.

9. Бутенин Н.В., Неймарк Ю.И., Фуфаев Н.А.: Введение в теорию нелинейных колебаний. М: "Наука", 1976, 384с.

10. Емельянов B.C.: Введение в системное моделирование. М:"Мир",1985, с.

11. Калман Р., Фалб П., Арбиб М.: Очерки по математической теории систем. М: "Мир", 1971, 700с.

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

13. Корноушенко Е.К.: Интервальные покоординатные оценки для множеств достижимых состояний линейной стационарной системы. В ж. Автоматика и телемеханика, 1980, N 5 с. 12-22, N 12 с.10-17.

14. Неймарк Ю.И.: Метод точечных отображений в теории нелинейных колебаний. М: "Наука", 1872, 471с.

15. Нестеров В.М.: Об одном обобщении интервального анализа и его применении для оценки множества значений функции. В сб. "Математические методы построения и анализа алгоритмов", с.109-124. Ленинград, "Наука", 1990г.

16. Первозванский А.А.: Курс теории автоматического управления. М: "Наука", 1986, 615с.

17. Прицкер А.: Введение в имитационное моделирование и язык СЛАМ И. М: "Мир", 1987, 646с.

18. Программное обеспечение моделирования непрерывно-дискретных систем, (под ред. В.Глушкова), М: "Наука", 1975.

19. Теория систем. Математические методы и моделирование. Сб. статей под ред. А.Колмогорова, С.Новикова. М: "Мир", 1989, 384с.

20. Черноусько Ф.Л.: Оценивание фазового состояния динамических систем. Метод эллипсоидов. М.: Наука, 1988, 320с.

21. Шокин Ю.И.: Интервальный анализ. Новосибирск, "Наука", 110с., 1981г.

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

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

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

25. Alur R., Fix L., Henzinger Т.A.: A Determinizable Class of timed Automata. Qth International Conference CAV'94. Lecture Notes in Сотр. Sci. 818, p.1-13, 1994.

26. Alur R., Courcoubetis C., Dill D.L.: Model-Checking for real-time systems. 5th LICS (5th IEEE Simp. Logic in Сотр. Sci.), p.414-425. IEEE Сотр. Soc. Press, 1990.

27. Alur R., Courcoubetis C., Henzinger Т., Ho P-T.: Hybrid automata: an algorithmic approach to the specification and analysis of hybrid systems. In Workshop on Theory of Hybrid Systems,Lyndby, Denmark, June 1993. LNCS 736, Springer-Verlag.

28. Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P.-H., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theoretical Сотр.Sc.,138, p.3-34, 1995.

29. Alur R, Feder T, Henzinger T.A.: The benefits of relaxing punctuality. In Proceeding of the Annual Symp. on Principles of Distributed Computing, p.139-152, ACM Press, 1991.

30. Alur R., Henzinger T.A., Ho P.-H.: Automatic symbolic verification of embedded dydtems. IEEE Transaction on Software Engineering, 22(3), p.181-201, 1996.

31. Asarin E., Maler O., Pnueli A.: Reachability Analysis of Dinamical Systems having Piecewise-Constant Derivatives. Theoretical Сотр. Sci., v.l38,N.l, 1995

32. Asarin E., Maler O.: On some Relations between Dynamical Systems and Transition Systems. Proc. of ICALP'94, Lecture Notes in Сотр. Sci 820, p.59-72, Springer-Verlag, 1994.

33. Bertolomieu В., Diaz M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, SE-17,N 3, March 1991.

34. Ben-Ari M., Manna, Z., Pnueli A.: The Temporal Logic of Branching Time. Proc. 8th Annual Symposium on Principles of Programming Languages, 1981, ACM Press, Williamsburg, p. 164-176, Springer-Verlag, 1992.

35. Bouajjani A., Robbana R.: Verifying w-regular properties for subclasses of linear hybrid systems. CAV, Springer LNCS, 1995.

36. Burch J.R., Ckarke E.M., McMillan K.L., Dill D.L., Hwang L.J.: Symbolic model checking: 1020 states and beyond. Informations and Computation, 98(2), p. 142-170, 1992.

37. Bryant R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), p.677-691, 1986.

38. Clarke E.M., Emerson E.A.: Design and synthesis of synchronisation skeletons using branching-time temporal logic. In Workshop on Logic of Program, Lecture Notes in Сотр.Sc. 131. Springer-Verlag, 1981.

39. Clarke E.M., Emerson E.A., Systla A.P.: Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2): p.244-263. 1986.

40. Emerson E.A., Clarke E.M.: Characterizing correctness properties of parallel programs as fixpoints. In ICALP 83: Automata, Languages and Programming, LNCS 85, p.169-181, Springer-Verlag, 1980.

41. Harel D.: Statecharts: a Visual Formalism for Complex Systems. Sci. Comput. Prog. 8, p.231-274, 1987.

42. Henzinger Т.A., Manna, Z., Pnueli A.: Temporal proof methodologies for real-time systems. Proc. 18th Annual Symposium on Principles of Programming Languages, 1991, ACM Press, p. 353-366.

43. Henzinger Т., Manna Z., Pnueli A.: Towards Refining Temporal Specifications into Hybrid Systems. In Hybrid Systems, LNCS 736, p.60-76, Springer-Verlag, 1993.

44. Henzinger Т., Nicollin X., Sifalis J., Yovine S.: Symbolic Model-Checking for Real-Time Systems. In Proc. 7th LICS. IEEE Сотр. Soc. Press, 1992.

45. Henzinger Т., Ho P-T.: HyTech: The Cornell Hybrid Technology Tool. Hybrid Systems II, Lecture Notes in Comp.Sci 999, p.265-293. Springer-Verlag, 1995.

46. Henzinger T.A., Ho P.-H.: Algorithmic analysis of nonlinear hybrid systems. CAV 95, Lecture Notes in Сотр. Sci. p. 225-238. Springer-Verlag, 1995.

47. Henzinger T.A., Wong-Toi H.: Using HyTech to synthesize control parameters for a steam boiler. Lecture Notes in Сотр. Sci. 1165, p. 265-282. Springer-Verlag, 1996.

48. Henzinger T.A., Ho P.-H., Wong-Toi H.: HyTech : a model checker for hybrid systems. Lecture Notes in Сотр. Sci. 1254, p. 460-463. Springer-Verlag, 1997.

49. T.A. Henzinger: Hybrid Automata with Finite Bisimulations. Lecture Notes in Сотр. Sci. 944, p. 324-335. Springer-Verlag, 1995.

50. Henzinger T.A., Корке P., Puri A., Varaiya P.: What's decidable about hybrid automata? ACM Symp. of Theory of Computing, p.373-382, 1995.

51. Ho P.-H.: Automatic Analysis of Hybrid Systems. PhD thesis, Cornell University, 1995.

52. Inichova M.A., Inichov D.B., Kolesov Y.B., NSenichenkov Y.B.: Movel Vision for Windows. Graphical environment for hybrid systwr simulating. User's Guade. Moscow-St.Petersburg, 1995.

53. Kesten Y., Pnueli A., Sifalis Y., Yovine S.: Integration Graph: a class of decidable hybrid systems. Hybrid Systems, Lecture Notes in Comp.Sci 736, p.179-208. Springer-Verlag, 1993.

54. Kolesov Y.B., Senichenkov Y.B.: Model Vision 3.0 for Windows 95/NT. The graphical environment for complex dynamic system design. ICI&C97 PROCEEDINGS, v.2, p.704-711, St.Petersburg, 1997.

55. Kolesov Y.B., Senichenkov Y.B.: Visual specification language intended for event-driven hierarchical dynamic system with variable structure. ICI&C97 PROCEEDINGS, v.2, p.712-719, St.Petersburg, 1997.

56. Lamport L.: Specifying concurrent program modules. ACM Trans. Prog. Lang. Syst. 5, p.190-222, 1983.

57. Lamport L.: What good is temporal logic. Proc.IFIP Congress,North-Holland, p.657-668, 1983.

58. Larsen K., Pettersson P., Yi W.: Compositional and symbolic model-checking of real-time systems, in Proceeding of the 16th Annual RealTime Systems Symposium, p.76-87, IEEE Сотр.Sc.Press, 1995.

59. Maler O., Manna Z., Pnueli A.: From Timed to Hybrid systems. RealTime: Theory in Practice, Lecture Notes in Comp.Sc 600, p.447-484. Springer-Verlag, 1992.

60. Manna Z., Pnueli A.: Verification of concurrent programs: A temporal proof system. Foundation of Comp.Sc 4, Distributed Systems: Part 2, Mathematical Centre Tracts 159, Center for Mathematics and Computer Science, Amsterdam, p.163-255, 1983.

61. Manna, Z., Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.

62. Manna Z., Pnueli A.: Verifying hybrid systems. Hybrid systems, LNCS 736, p.4-35, Springer-Verlag, 1993.

63. McManis J., Varajya P.: Suspension Automata: A Decidable Class of Hybrid Automata. 6th International Conference CAV'94. Lecture Notes in Сотр. Sci. 818, p.105-117, 1994.

64. Nicollin X., Olivero A., Sifalis Y., Yovine S.: An Approach to the Description and Analysis of Hybrid Systems. Hybrid Systems, Lecture Notes in Сотр.Sci 736, p. 149-178. Springer-Verlag, 1993.

65. Olivero A., Yovine S.: Kronos: a tool for verifying real-time systems. User's Guide and Reference Manual. VERIMAG, Grenoble, France, 1992.

66. Olivero A., Sifakis J., Yovine S.: Using Abstractions for the Verification of Linear Hybrid Systems. 6*/i International Conference CAV'94. Lecture Notes in Сотр. Sci. 818, p.81-94, 1994.

67. Pnueli A., Rosner R. On the synthesis of a reactive module. Technical report, Weizmann Institute of Dcience, 1988.

68. Puri A., Varajya P.: Decidability of Hybrid Systems with Rectangular Differential Inclusions. 6fh International Conference CAV'94. Lecture Notes in Сотр. Sci. 818, p.95-104, 1994.

69. Stauner Т., Muller O., Fuchs M.: Using Ну Tech to verify an automotive control system. Lecture Notes in Сотр. Sci. 1201, p. 139-153. Springer-Verlag, 1997.

70. Wong-Toi H.: Symbolic approximations for verifying real-time systems. PhD thesis, Standford University, 1994.

71. Wolfram S.: Mathematical A System for Doing Mathematics by Computer. Addisson-Wesley Publishing Company, 1988.

72. Redfern D.: The Maple Handbook. 531 pp., Springer-Verlag, 1994.

73. SIMULINK. The ultimate simulation environment. MathWorks, 1994.