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

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

Автор: Парийская, Екатерина Юрьевна

Автор: Парийская, Екатерина Юрьевна

Шифр специальности: 05.13.17

Научная степень: Кандидатская

Год защиты: 2000

Место защиты: Ярославль

Количество страниц: 160 с. ил.

Артикул: 296823

Стоимость: 250 руб.

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

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. Манны и других современных авторов , , , , , для решения задач моделирования и анализа дискретных параллельных и распределенных систем. Элементами дискретной параллельной системы являются дискретные системы называемые процессами, параллельно функционирующие в дискретном времени. Параллелизм является отражением либо физического аппаратного параллелизма одновременной работы нескольких физических устройств, либо логического параллелизма концептуального параллелизма, введенного человеком, независимо от того, происходит ли работа процессов последовательно или параллельно.

Рекомендуемые диссертации данного раздела

28.06.2016

+ 100 бесплатных диссертаций

Дорогие друзья, в раздел "Бесплатные диссертации" добавлено 100 новых диссертаций. Желаем новых научных ...

15.02.2015

Добавлено 41611 диссертаций РГБ

В каталог сайта http://new-disser.ru добавлено новые диссертации РГБ 2013-2014 года. Желаем новых научных ...


Все новости

Время генерации: 0.204, запросов: 244