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

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

Содержание
Введение

Глава 1. Автоматное программирование для решения задач логического управления

1.1. Автоматное программирование или йисИтсхнология

1.2. Проблема верификации автоматных программ.

1.3. Синхронный подход

1.4. Синхронный подход в языке свЬсге .

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

2.1. Формальная модель автоматной программы

2.2. Форматы данных

2.3. Верифицируемые свойства. Язык ТетрЕй

2.4. Структура среды разработки.
Глава 3. Примеры
3.1. Пример 1 Арбитр шины .
3.2. Пример 2 Часыбудильник.
3.3. Пример 3 Микроволновая печь
3.4. Выводы.
Заключение
Литература


Одним из развитий иерархической модели автоматных программ [] является модель [9], использующая формализм сетей Петри. Разработка программы выполняется в UniMod, применяется верификатор CPN/Tools [], рассмотрен пример системы управления кофеваркой. Получено свидетельство об официальной регистрации программы для ЭВМ []. На кафедре технологий программирования СПбГУ ИТМО были получены в том числе следущис результаты [. В работе [7] рассматривается техника верификации автоматных программ, состоящих из одного конечного автомата. Описывается преобразование автомата в структуру Крнпкс, выражение темпоральных свойств на языке CTL, верификация по модели (метод “Model Checking”) и построение сценария для исходного автомата, если был найден контрпример. Техника верификации демонстрируется на примере универсального инфракрасного пульта для бытовой техники [8]. Применение метода Model Checking также исследуется в работах |5, 6]. Можно заметить, что все авторы используют Model Checking. Главное различие наблюдается в моделях. Данная работа не является исключением. Наиболее обстоятельное описание АП можно найти в книге []. Она была взята за основу. В указанном источнике предполагается, что входные сигналы автомата могут только бинарными. Во многих подходах разрешается использовать целые и вещественные числа в качестве значений входных сигналов. Логические сигналы оставляют разработчику меньше свободы, по они ближе к решаемой задаче, задаче логического управления. Язык синхронного программирования estercl разрабатывался для аналогичного круга задач, что и автоматное программирование. В отличие от АП, в estercl был изначально заложен прочный теоретический фундамент. В este-rel существует базис — подмножество языка, на котором можно определить все его операторы. Программа на языке esterel — это уже модель, готовая для верификации. Существует верификатор Xcve для проверки esterel программ. АП и язык esterel помимо общей задачи роднит тот факт, что оба они используют бинарные сигналы. Esterel допускает сигналы с дополнительными значениями. Однако значения не используются в процессе верификации, только сггатус сигнала (“true” — “false” или “присутствует” — “отсутствует”) принимается во внимание. АП и esterel удачно дополняют друг друга. АП предлагает средства для визуальной разработки программ, a estercl обеспечивает прочную математическую основу и средства верификации. Xeve — это верификатор для esterel программ, представляемых в виде конечных автоматов. Xcve предлагает дружественный графический пользовательский интерфейс. Компилятор языка estercl преобразует программу в систему в систему логических уравнений с защелками (latch), которые неявно определяют конечный автомат. Xeve работает с неявно заданным конечным автоматом. Внутри верификатора автомат описывается с помощью бинарных диаграмм решений (Binary Decision Diagrams). Верификатор Xeve был разработан совместно институтом Inria1 и Ecole des Mines de Paris2 в рамках исследовательского проекта TICK3. Технология оказалось многообещающей. Выло решено адаптировать ее для промышленного использования. Так появилась компания Estercl Technologies. Сейчас Esterel Techonlogics может гордиться удачными проектами со многими известными заказчиками: Airbus, Elbit Systems, Intertechnique, Eurocoptcr и др4. Цель диссертационной работы Главная цель диссертации — создать программный комплекс разработки и верификация автоматных программ. Достижение указанной цели было связано с решением следующих подзадач. Разработать формальную модель автоматной программы, которая бы подходила для сложившейся практики применения автоматного программирования. Разработать метод верификации автоматных программ. Разработать и реализовать программные средства построения и верификации автоматных программ. Исследовать работу программной системы при решении практических задач. Научная новизна Все основные результаты являются новыми. Разработана формальная модель автоматной программы, учитывающая наиболее важные идеи автоматного программирования. К автоматному программированию был применен синхронный подход. Уточнена временная модель.