Руководитель проекта – А. А. Шалыто Докладчик – Ф. Н. Царев презентация

Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Руководитель проекта – А. А. Шалыто Докладчик – Ф. Н. Царев

Парадигма автоматного программирования Предложено в России в 1991 году Программные системы разрабатываются как системы взаимодействующих автоматизированных объектов управления Система управления является системой взаимодействующих конечных автоматов

Виды верификации Динамическая Тестирование Статическая Доказательная Верификация на модели

Верификация моделей традиционно построенных программ Модель поведения программы строится на этапе верификации Построение модели Крипке соответствие модели программе Построение формальных требований формулировка требований в терминах модели Крипке Формальная верификация большая размерность пространства состояний Отображение контрпримеров преобразования контрпримеров в термины исходной программы

Верификация автоматной модели программы Модель поведения программы (в общем случае, система взаимосвязанных автоматов) строится не на этапе верификации, а при проектировании программы Формальное построение модели для верификации по модели поведения возможность автоматизации Формулировка требований к программе в терминах автоматов Формальная верификация рассмотрение управляющих состояний Формальное восстановление контрпримеров в терминах исходной модели – модели поведения

Предлагаемые методы Метод верификации автоматных программ с использованием верификатора NuSMV Метод верификации на основе темпоральной логики CTL Метод верификации визуальных автоматных моделей Метод верификации на основе эмуляции

1. Метод верификации автоматных программ с использованием верификатора NuSMV Выделение промежуточных состояний в каждом автомате Запись каждого автомата набором переменных и переходов между ними Объединение моделей автоматов в общую модель

Выделение промежуточных состояний (метод 1) s1 – автомат находится в состоянии s1; s2 – в этом состоянии модели автомат вызывает автомат A2 с событием e1; s3 – переходит в основное состояние s2; s5 – автомат находится в состоянии s2

Запись требований (метод 1) Формулы темпоральной логики ACTL Автомат Ak находится в состоянии sj – yk.sj. Выполнилось выходное воздействие z1 – Action_z1. Произошло событие ei – A1.ei Темпоральные операторы: AF, AG, A[U]

Инструментальное средство FSM Verifier (метод 1) Вход – система автоматов Мили Преобразует систему автоматов в модель для верификатора NuSMV Преобразует контрпример из формата NuSMV в термины исходной системы автоматов

2. Метод верификации на основе темпоральной логики CTL Рекурсивное построение модели Крипке для системы автоматов, взаимодействующих через вложенность Выделение промежуточных состояний в каждом автомате: промежуточные состояния, построенные из выходных воздействий промежуточные состояния на переходах

Промежуточные состояния (метод 2)

Запись требований (метод 2) Требования записываются в виде CTL-формул Темпоральные операторы: AF, AG, A[U], AX, EF, EG, E[U], EX

Инструментальное средство CTL Verifier (метод 2) Вход – система смешанных (Мили-Мура) автоматов, взаимодействующих по вложенности Преобразует систему автоматов в модель Крипке Выполняет верификацию (алгоритм Кларка-Эмерсона-Систлы) Преобразует контрпример из терминов модели Крипке в термины исходной модели

3. Метод верификации визуальных автоматных моделей Преобразование автоматной модели в текст программы на языке Promela Для каждого автомата создается функция, для текущего состояния переменная, для каждого перехода – оператор, … (14 правил) Требования записываются в виде LTL-формул Операторы G, F, U

Верификация с применением SPIN (метод 3)

Инструментальное средство Converter (метод 3) Вход – XML-описание автоматной модели, построенной в UniMod Преобразование автоматной модели в текст программы на языке Promela Верификация программы с помощью верификатора SPIN Отображение контрпримера в терминах модели на языке Promela

4. Метод верификации на основе эмуляции Глобальное состояние автоматной программы задается набором состояний ее автоматов. Элементарным шагом программы является обработка автоматной программой одного события. Элементарный шаг откатывается путем установки автоматов в исходные состояния. Перебор возможных историй работы программы происходит за счет выбора всех возможных событий и выбора всех возможных значений условий на переходах. Предикаты описывают события, действия и значения переменных, полученные в последнем шаге. Требования записываются в виде LTL-формул Операторы G, F, U

Верификация с применением Bogor (метод 4)

Инструментальное средство UniMod.Verifier (метод 4)

Пример применения метода 4 – модель банкомата

Банкомат выдает деньги только после авторизации [не выдадут деньги] U [введет правильный PIN-код] !o1.z10 U e10 LTL.temporalProperty( Property.createObservableDictionary( Property.createObservableKey("correct_pin", AutomataModel.wasEvent(model, "e10")), Property.createObservableKey("give_money", AutomataModel.wasAction(model, "o1.z10")) ), LTL.weakUntil( LTL.negation(LTL.prop("give_money")), LTL.prop("correct_pin") ) ); Свойство выполняется

Деньги не выдаются, пока пользователь не сделает соответствующий запрос [не выдаются деньги] U [сделан запрос на выдачу денег] !o1.z10 U e23 LTL.temporalProperty ( Property.createObservableDictionary ( Property.createObservableKey("money_requested", AutomataModel.wasEvent(model, "e23")), Property.createObservableKey("give_money", AutomataModel.wasAction(model, "o1.z10")) ), LTL.weakUntil ( LTL.negation(LTL.prop("give_money")), LTL.prop("money_requested") ) ); Свойство не выполняется

Результаты Разработаны четыре метода верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Эффективность методов продемонстрирована на задаче верификации модели банкомата Разработаны прототипы программных средств, поддерживающих указанные методы

Выполнение программных индикаторов Защищена одна диссертация на соискание ученой степени кандидата технических наук – Гуров В. С. Технология проектирования и реализации объектно-ориентированных программ с явным выделением состояний (метод, инструментальное средство, верификация) Опубликовано восемь статей в ведущих научных журналах Получено четыре свидетельства об официальной регистрации программы для ЭВМ

Спасибо за внимание