'

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

Понравилась презентация – покажи это...





Слайд 0

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


Слайд 1

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


Слайд 2

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


Слайд 3

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


Слайд 4

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


Слайд 5

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


Слайд 6

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


Слайд 7

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


Слайд 8

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


Слайд 9

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


Слайд 10

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


Слайд 11

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


Слайд 12

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


Слайд 13

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


Слайд 14

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


Слайд 15

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


Слайд 16

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


Слайд 17

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


Слайд 18

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


Слайд 19

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


Слайд 20

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


Слайд 21

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


Слайд 22

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


Слайд 23

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


Слайд 24

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


Слайд 25

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


×

HTML:





Ссылка: