Верификация автоматных программ

• Автор: Лукин, Михаил Андреевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2014
• Место защиты: Санкт-Петербург
• Количество страниц: 185 с. : ил.

Оглавление
Оглавление
Введение

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

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

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

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

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

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

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

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

Апробация диссертации
Публикации
Структура диссертации
Г лава 1. Основные понятия
1.1. Конечный автомат
1.2. Автоматы Мили и Мура
1.3. Структурные авто маты
1.4. Верификация
1.5. Темпоральная логика
1.6. Модель Крипке
1.7. Автомат Бюхи
1.8. Автоматные программы
Выводы по главе

Глава 2. Обзор методов верификации автоматных программ разных типов
2.1. Сравнение с аналогами
Выводы по главе
Глава 3. Описание предлагаемого метода
3.1. Описание автоматной модели
3.1.1. Математическая модель управляющего автомата
3.1.2. Математическая модель вложенных автоматов
3.1.3. Математическая модель параллельно работающих автоматов
3.2. Описание предложенного метода верификации
3.2.1. Построение 5д>ш-модели для управляющего автомата
3.2.2. Построение Spin-модели для вложенных автоматов
3.2.3. Построение Sp/я-модели для параллельных автоматов
3.2.4. Преобразование LTL-формул
3.2.5. Запуск верификатора Spin
3.2.6. Преобразование контрпримера
3.2.7. Интерактивность
3.3. Генерация программного кода
3.3.1. Первичная генерация кода
3.3.2. Повторная генерация кода
3.4. Верификация автоматов Stateflow
3.5. Верификация автоматов стандарта IEC 61
3.5.1. Верификация базовых функциональных блоков
3.5.2. Верификация составных функциональных блоков
3.6. Описание метода верификации однопоточных автоматов и
инструментального средства Converter

3.6.1. Описание метода
3.6.2. Описание инструментального средства Converter
3.7. Описание инструментального средства Stater
3.7.1. Описание интерфейса Stater
3.7.2. Генерация кода
3.7.3. Верификация
3.7.4. Архитектура Stater
3.8. Верификация параллельной системы автоматов, управляющих
гусеничным шасси
Выводы по главе
Г лава 4. В недрение
4.1. Инструментальное средство Converter
4.2. Инструментальное средство Stater
4.2.1. Загрузка из XML-файла
4.2.2. Игра Turtleball
4.2.3. Программа Memory cards для запоминания иностранных слов
Выводы по главе
Глава 5. Подход к верификации программ в случае, когда модель внешней среды нельзя представить в виде автомата
5.1. Формулировка задачи
5.2. Предлагаемый подход к верификации
5.3. Гипотеза
5.4. Построение модели
5.5. LTL-спецификация
5.6. Доказательство корректности алгоритмов

пятой главе, имеют более 107 состояний и занимают более 800 Мб памяти каждая.
Для того чтобы уменьшить модель, в работе предлагается строить её интерактивно. Для этого вводится возможность выбирать, какие уровни абстракции автоматной системы входят в модель, а какие нет. Также модель структурируется понятным для человека образом для того, чтобы пользователь мог самостоятельно модифицировать построенную модель.
Подразделы этого раздела описывают компоненты 5/л'и-моделей, обеспечивающие интерактивность.
3.2.7.1. Переменные
Для переменных введём следующие уровни абстракции:
1. Переменные в модели не учитываются.
2. Переменные в модель включены, но модель абстрагируется от их значения. Недетерминированно выбирается, какое охранное условие будет верно.
3. Модель вычисляет значения переменных. При этом переменные могут быть следующих видов:
a. Локальные. Эти переменные могут быть изменены только самим конечным автоматом. Все изменения таких переменных находятся только в выходных воздействиях автомата.
b. Публичные. Такие переменные могут быть изменены в любом месте программы, в которую входит система иерархических автоматов. В модели перед каждым переходом автомата каждой такой переменной недетерминированно присваивается произвольное значение.
c. Совместно используемые. К таким переменным автомата имеют доступ другие автоматы, параллельно работающие с данным.
б. Параметры. Извне изменяются только один раз, при запуске автомата. В остальном они подобны локальным.