Оглавление

Оглавление........................................................................................................ 2

Введение............................................................................................................

Актуальность................................................................................................ 6

Цель диссертационной работы.................................................................... 6

Методы исследования.................................................................................. 7

Научная новизна........................................................................................... 7

Достоверность.............................................................................................. 7

Практическое значение................................................................................. 8

Экспериментальные исследования............................................................... 8

Использование и внедрение результатов работы........................................ 8

Апробация диссертации............................................................................... 9

Публикации................................................................................................ 10

Структура диссертации............................................................................... 10

Глава 1. Основные понятия........................................................................... 11

1.1. Конечный автомат............................................................................. 11

1.2. Автоматы Мили и Мура................................................................... 11

1.3. Структурные автоматы..................................................................... 12

1.4. Верификация.....................................................................................

1.5. Т емпоральная логика....................................................................... 15

1.6. Модель Крипке................................................................................. 16

1.7. Автомат Бюхи................................................................................... 18

1.8. Автоматные программы................................................................... 19

Выводы по главе 1..................................................................................... 19

Глава 2. Обзор методов верификации автоматных программ разных типов ... 19

2.1. Сравнение с аналогами..................................................................... 19

Выводы по главе 2..................................................................................... 22

Глава 3. Описание предлагаемого метода...................................................... 23

3.1. Описание автоматной модели.......................................................... 23

3.1.1. Математическая модель управляющего автомата..................... 23

3.1.2. Математическая модель вложенных автоматов........................ 24

3.1.3. Математическая модель параллельно работающих автоматов.... 25

3.2. Описание предложенного метода верификации.............................. 26

3.2.1. Построение Spin-модели для управляющего автомата.............. 26

3.2.2. Построение Spin-модели для вложенных автоматов................ 29

3.2.3. Построение Spin-модели для параллельных автоматов............ 29

3.2.4. Преобразование LTL-формул.................................................... 33

3.2.5. Запуск верификатора Spin.......................................................... 34

3.2.6. Преобразование контрпримера.................................................. 34

3.2.7. Интерактивность......................................................................... 34

3.3. Генерация программного кода ........................................................

3.3.1. Первичная генерация кода......................................................... 38

3.3.2. Повторная генерация кода......................................................... 38

3.4. Верификация автоматов Stateflow.................................................... 42

3.5. Верификация автоматов стандарта IEC 61499................................. 43

3.5.1. Верификация базовых функциональных блоков...................... 43

3.5.2. Верификация составных функциональных блоков................... 46

3.6. Описание метода верификации однопоточных автоматов и

инструментального средства Converter...................................................... 47

3.6.1. Описание метода......................................................................... 48

3.6.2. Описание инструментального средства Converter..................... 54

3.7. Описание инструментального средства Stater.................................. 60

3.7.1. Описание интерфейса Stater........................................................ 60

3.7.2. Генерация кода........................................................................... 72

3.7.3. Верификация.............................................................................. 73

3.7.4. Архитектура Stater..................................................................... 75

3.8. Верификация параллельной системы автоматов, управляющих

гусеничным шасси..................................................................................... 77

Выводы по главе 3..................................................................................... 79

Глава 4. Внедрение......................................................................................... 81

4.1. Инструментальное средство Converter............................................. 81

4.2. Инструментальное средство Stater................................................... 81

4.2.1. Загрузка из XML- файла.............................................................

4.2.2. Игра Turtleball............................................................................ 84

4.2.3. Программа Memory cardsдля запоминания иностранных слов... 87

Выводы по главе 4..................................................................................... 92

Глава 5. Подход к верификации программ в случае, когда модель внешней

среды нельзя представить в виде автомата..................................................... 93

5.1. Формулировка задачи...................................................................... 93

5.2. Предлагаемый подход к верификации.............................................. 96

5.3. Гипотеза............................................................................................ 97

5.4. Построение модели ........................................................................ 98

5.5. LTL-спецификация............................................................................ 99

5.6. Доказательство корректности алгоритмов ................................... 115

5.7. Результаты верификации

117

Выводы по главе 5

118

Заключение

119

Источники

120

Приложение А. Модель и вывод Spinпри верификации программы

AntSysEditor................................................................................................... 127

Приложение Б. Модель и вывод Spinпри верификации логики в игре Tutrleball

....................................................................................................................... 152