Генерация управляющих автоматов на основе генетического программирования и верификации

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

ОГЛАВЛЕНИЕ
Введение

Глава 1. Автоматное программирование и верификация автоматных программ

1.1. Автоматное программирование

1.1.1. Технология автоматного программирования

1.1.2. Управляющий конечный автомат

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

1.2.1. Традиционная верификация моделей на основе метода

Model Checking

1.2.2. Особенности верификации автоматных программ

Выводы по главе
Глава 2. Применение генетического программирования и верификации для построения автоматов
2.1. Модификация метода построение автоматов по темпоральным формулам и тестовым примерам
2.1.1. Входные и выходные данные
2.1.2. Особь алгоритма генетического программирования
2.1.3. Функция приспособленности
2.1.4. Мутация
2.1.5. Скрещивание
2.2. Модификации алгоритма построения автоматов на основе генетического программирования и верификации
2.2.1. Построение автоматов по контрактам
2.2.2. Сценарии работы
2.3. Экспериментальные исследования
2.3.1. Автомат управления дверьми лифта
2.3.2. Автомат управления часами с будильником

Выводы по главе
Глава 3. Технология построения автоматных программ на основе генетического программирования и верификации
3.1. Верификация автоматных программ и верификатор AutomataVerificator
3.2. Построение автоматных программ на основе генетического программирования по тестам
3.3. Технология создания автоматных программ на основе генетического программирования и верификации
3.4. Инструментальное средство для поддержки технологии генерации автоматов на основе генетического программирования и верификации
3.4.1. Использование инструментального средства
Выводы по главе
Глава 4. Внедрение результатов работы при построении модулей для программного продукта NetFlow Integrator
4.1. Принцип работы приложения NetFlow Integrator
4.1.1. Правила обработки iVe/F/ow-сообщений
4.1.2. Граф представления модуля
4.2. Построение модуля для NetFlow Integrator на основе генетического программирования и верификации
4.2.1. Описание объектов управления
4.2.2. Входные и выходные воздействия
4.2.3. Спецификация модуля
4.2.4. Результаты построения модуля
Выводы по главе
Заключение
Список источников
Печатные издания на русском языке
Печатные издания на английском языке

Ресурсы сети Интернет
Публикации автора
Статьи в журналах из перечня ВАК
Другие статьи автора
Материалы конференций с участием автора
Приложение 1. XML-описание данных для экспериментов по генерации
автомата управления дверьми лифта
Приложение 2. UniMod-моделъ автомата управления дверьми лифта
Приложение 3. ZMZ-описание данных для экспериментов по генерации
модуля Top traffic monitor
Приложение 4. UniMod-моделъ автомата управления модулем Top traffic monitor

создании автоматной модели на основе тестов, такой переход считается отличным от перехода просто по событию Т без условий.
Однако, оба перехода (с условием и без него) идентичны для предиката по событию - \’а5Еуеп!(Т) («переход совершен по событию 7>>). При верификации, если переход был совершен по событию Т или этому же событию, но с некоторым условием, то в обоих случаях данный предикат будет выполнен. Заметим, что можно вводить предикаты и на условия на переходах, тогда такие переходы будут отличаться и для верификатора. Например, можно добавить предикат мазТгие(х1) (условие х1 верно), тогда он не будет выполняться на переходе Т [!х1 && х2], но будет верен для перехода Т [х1 && х2].
2.1.2. Особь алгоритма генетического программирования
В настоящей работе используется такое же представление автоматов в виде особи алгоритма генетического программирования, как и в работах [18,19, 52].
Особь при генетическом программировании представлена автоматом, который содержит список переходов для каждого из состояний и номер начального состояния. Переходы задаются событиями и числом выходных воздействий, которые необходимо вызвать у объекта управления.
Таким образом, в особи кодируется только «скелет» (рисунок 4) автомата, а конкретные выходные воздействия, вырабатываемые на переходах, определяются с помощью алгоритма расстановки пометок [18].