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

подхода

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

Санкт-Петербургский государственный университет информационных технологий, механики и оптики

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

Состояния
События и входные переменные
Выходные воздействия
Конечный автомат
Система конечных автоматов

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

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

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

промежуточных состояний в каждом автомате
Запись каждого автомата набором переменных и переходов между ними
Объединение моделей автоматов в общую модель

состоянии s1;
s2 – в этом состоянии модели автомат вызывает автомат A2 с событием e1;
s3 – переходит в основное состояние s2;
s5 – автомат находится в состоянии s2

в состоянии sj – yk.sj.
Выполнилось выходное воздействие z1 – Action_z1.
Произошло событие ei – A1.ei
Темпоральные операторы: AF, AG, A[U]

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

модели Крипке для системы автоматов, взаимодействующих через вложенность
Выделение промежуточных состояний в каждом автомате:
промежуточные состояния, построенные из выходных воздействий
промежуточные состояния на переходах

состояния на переходах

AF, AG, A[U], AX, EF, EG, E[U], EX

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

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

построенной в UniMod
Преобразование автоматной модели в текст программы на языке Promela
Верификация программы с помощью верификатора SPIN
Отображение контрпримера в терминах модели на языке Promela

задается набором состояний ее автоматов.
Элементарным шагом программы является обработка автоматной программой одного события.
Элементарный шаг откатывается путем установки автоматов в исходные состояния.
Перебор возможных историй работы программы происходит за счет выбора всех возможных событий и выбора всех возможных значений условий на переходах.
Предикаты описывают события, действия и значения переменных, полученные в последнем шаге.
Требования записываются в виде LTL-формул
Операторы G, F, 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")
)
);
Свойство не выполняется

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

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