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

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

3 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Виды верификации Динамическая Тестирование Статическая Доказательная Верификация на модели

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

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

6 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Предлагаемые методы 1. Метод верификации автоматных программ с использованием верификатора NuSMV 2. Метод верификации на основе темпоральной логики CTL 3. Метод верификации визуальных автоматных моделей 4. Метод верификации на основе эмуляции

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

8 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Выделение промежуточных состояний (метод 1) s1 – автомат находится в состоянии s1; s2 – в этом состоянии модели автомат вызывает автомат A2 с событием e1; s3 – переходит в основное состояние s2; s5 – автомат находится в состоянии s2

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

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

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

12 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Промежуточные состояния (метод 2) Промежуточные состояния, построенные из выходных воздействий Промежуточные состояния на переходах

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

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

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

16 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Верификация с применением SPIN (метод 3)

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

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

19 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Верификация с применением Bogor (метод 4)

20 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Инструментальное средство UniMod.Verifier (метод 4)

21 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Пример применения метода 4 – модель банкомата Автомат AClient Автомат AServer

22 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Банкомат выдает деньги только после авторизации [не выдадут деньги] 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") ) ); Свойство выполняется

23 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Деньги не выдаются, пока пользователь не сделает соответствующий запрос [не выдаются деньги] 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") ) ); Свойство не выполняется

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

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

26 Технология верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода Спасибо за внимание