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

• Автор: Парийская, Екатерина Юрьевна
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 2000
• Место защиты: Ярославль
• Количество страниц: 160 с. : ил.

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

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

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

подхода.

1.3 Классификация и спецификация свойств поведения в

дискретном темпоральном подходе, темпоральная логика

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

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 Метод покоординатных оценок. Функция .
2.4.1 Постановка задачи и обоснование решения .
2.4.2 Описание метода покоординатных оценок
2.4.3 Функция x для метода покоординатных
оценок4
2.4.4 Теорема о точности метода покоординатных оценок
2.4.5 Замечание о методе покоординатных оценок . .
2.5 Метод оценки временного интервала. Функция 1
2.5.1 Постановка задачи и описание метода.
2.5.2 Теорема о точности метода оценки временного интервала
Заключение
Список литературы


Представлена базовая математическая модель дискретной параллельной системы система переходов, две основные модели дискретных систем реального времени система временных переходов и таймированный автомат, которые лежат в основе гибридного направления и метода символьной верификации гибридных систем. Представлена классификация требований к поведению дискретных параллельных систем, которые могут быть верифицированы в рамках дискретного темпорального подхода, и базовый язык спецификаций требований к поведению темпоральная логика. Далее подробно представлен метод символьной верификации и два алгоритма линейной аппроксимации гибридных автоматов. Рассмотрены примеры верификации и линейной аппроксимации гибридных автоматов, описаны недостатки существующих алгоритмов линейной аппроксимации. Рассматриваемый в настоящей работе гибридный подход к исследованию непрерывнодискретных систем является развитием дискретного темпорального подхода, развитого в работах А. Пнуэли, Д. Харела, Е. Кларка, Е. Эмерсона, 3. Манны и других современных авторов , , , , , для решения задач моделирования и анализа дискретных параллельных и распределенных систем. Элементами дискретной параллельной системы являются дискретные системы называемые процессами, параллельно функционирующие в дискретном времени. Параллелизм является отражением либо физического аппаратного параллелизма одновременной работы нескольких физических устройств, либо логического параллелизма концептуального параллелизма, введенного человеком, независимо от того, происходит ли работа процессов последовательно или параллельно.