Автор: Вельдер С. Э., аспирант Руководитель: Шалыто А. А., доктор технических наук, профессор, заведующий кафедрой «Технологии программирования» Верификация автоматных моделей на основе построения редуцированного графа переходов СПбГУ ИТМО, кафедра компьютерных технологий, 2009 г.

Постановка задачи 2 / 17 1.Требуется предложить эффективный метод верификации программ, построенных на основе автоматного подхода. Этапами верификации должны быть такие преобразования: Автоматная модель модель Крипке алгоритм верификации путь в модели Крипке путь (подробный) в исходном автомате. 2.Реализовать метод в инструментальном средстве для ЭВМ и применить его для верификации конкретных приложений. Трассы, построенные программой, должны однозначно отображаться из модели Крипке в автомат.

Model checking 3 / 17

Семантика CTL 4 / 17

Преимущества автоматных программ при верификации 5 / 17 Модели программ, создаваемые на основе Switch-технологии, могут быть эффективно проверены, так как в таких программах управляющие состояния явно выделены, а их количество обозримо. Это позволяет строить компактные модели Крипке даже для программ большой размерности. Программа, спроектированная на основе автоматного подхода, является хорошим приближением к модели Крипке.

Вынесение выходных воздействий в отдельные состояния 6 / 17

Обработка автоматов, вложенных в состояние 7 / 17

Обработка переходов: выделение всех возможных комбинаций входных воздействий 8 / 17

Обработка переходов: построение редуцированного графа 9 / 17

Пример построения модели: внешний автомат 10 / 17

Пример построения модели: вложенный автомат 11 / 17

Пример построения модели: модель Крипке 12 / 17

Построение контрпримера 13 / 17

Контрпример в исходной модели: внешний автомат 14 / 17

Контрпример в исходной модели: вложенный автомат 15 / 17

Общий вид контрпримера или подтверждающей трассы 16 / 17 Если есть хотя бы один путь, подтверждающий свойство, то найдётся соответствующий путь вида αβ ω.

Заключение. Результаты 17 / 17 1.Предложены методы моделирования (конвертации автомата в модель Крипке) и спецификации, однозначно отражающие поведение автомата, позволяющие различать состояния, события и выходные воздействия в формулах темпоральных логик. 2. Получено свидетельство о регистрации программы для ЭВМ, в которой реализован алгоритм верификации и построения контрпримеров. Контрпримеры имеют вид смешанной периодической последовательности состояний и отображаются однозначно из модели Крипке в автомат. 3. Предлагаемый подход апробирован на примерах автоматных моделей программ, таких как модель поведения инфракрасного пульта ДУ и модель банкомата (НИР, выполняемая по гос. контракту от ).