Скачать презентацию
Идет загрузка презентации. Пожалуйста, подождите
1
Автор: Вельдер С. Э., аспирант Руководитель: Шалыто А. А., доктор технических наук, профессор, заведующий кафедрой «Технологии программирования» Верификация автоматных моделей на основе построения редуцированного графа переходов СПбГУ ИТМО, кафедра компьютерных технологий, 2009 г.
2
Постановка задачи 2 / 17 1.Требуется предложить эффективный метод верификации программ, построенных на основе автоматного подхода. Этапами верификации должны быть такие преобразования: Автоматная модель модель Крипке алгоритм верификации путь в модели Крипке путь (подробный) в исходном автомате. 2.Реализовать метод в инструментальном средстве для ЭВМ и применить его для верификации конкретных приложений. Трассы, построенные программой, должны однозначно отображаться из модели Крипке в автомат.
3
Model checking 3 / 17
4
Семантика CTL 4 / 17
5
Преимущества автоматных программ при верификации 5 / 17 Модели программ, создаваемые на основе Switch-технологии, могут быть эффективно проверены, так как в таких программах управляющие состояния явно выделены, а их количество обозримо. Это позволяет строить компактные модели Крипке даже для программ большой размерности. Программа, спроектированная на основе автоматного подхода, является хорошим приближением к модели Крипке.
6
Вынесение выходных воздействий в отдельные состояния 6 / 17
7
Обработка автоматов, вложенных в состояние 7 / 17
8
Обработка переходов: выделение всех возможных комбинаций входных воздействий 8 / 17
9
Обработка переходов: построение редуцированного графа 9 / 17
10
Пример построения модели: внешний автомат 10 / 17
11
Пример построения модели: вложенный автомат 11 / 17
12
Пример построения модели: модель Крипке 12 / 17
13
Построение контрпримера 13 / 17
14
Контрпример в исходной модели: внешний автомат 14 / 17
15
Контрпример в исходной модели: вложенный автомат 15 / 17
16
Общий вид контрпримера или подтверждающей трассы 16 / 17 Если есть хотя бы один путь, подтверждающий свойство, то найдётся соответствующий путь вида αβ ω.
17
Заключение. Результаты 17 / 17 1.Предложены методы моделирования (конвертации автомата в модель Крипке) и спецификации, однозначно отражающие поведение автомата, позволяющие различать состояния, события и выходные воздействия в формулах темпоральных логик. 2. Получено свидетельство о регистрации программы для ЭВМ, в которой реализован алгоритм верификации и построения контрпримеров. Контрпримеры имеют вид смешанной периодической последовательности состояний и отображаются однозначно из модели Крипке в автомат. 3. Предлагаемый подход апробирован на примерах автоматных моделей программ, таких как модель поведения инфракрасного пульта ДУ и модель банкомата (НИР, выполняемая по гос. контракту от ).
Еще похожие презентации в нашем архиве:
