Верификация автоматных программ Ремизов А.О., д.т.н., проф. Шалыто А.А. - презентация

1 Верификация автоматных программ Ремизов А.О., д.т.н., проф. Шалыто А.А.

2 2 Методы верификации программного обеспечения Экспертиза Статический анализ Динамические методы Формальные методы Синтетические методы

3 3 Верификация методом Model checking 1.Построение формальной модели 2.Формулировка требований к программе и модели с помощью формул темпоральной логики 3.Инструментальное средство верификации (например, SPIN) 4.Верификация модели

4 4 Трудности верификации традиционных программ Отсутствие автоматического преобразования в модель для верификации Отсутствие автоматического перехода от контрпримера к программе Генерация огромного числа состояний структуры Крипке

5 5 Верификация автоматных программ с помощью верификатора SPIN 1.Автоматическое преобразование автомата в текстовое описание модели (структуру Крипке) на языке Promela 2.Число состояний (управляющих) от единиц до сотен (тысяч) 3.Задание отрицания проверяемого требования формулой темпоральной логики и генерации для нее конструкции never claim 4.Преобразование текстового описания модели на языке Promela с включенной конструкцией never claim в программу на языке C 5.Верификация модели 6.Вывод контрпримера (в случае ошибки) и автоматический переход к контрпримеру в программе

6 6 Парадигма автоматного программирования СУОУ z1z1 x 2, e x1x1 Автоматизированный объект управления Устройство управления a b c Машина Тьюринга

7 7 Схема связей Пример. Начальная загрузка модуля борьбы с противником

8 8 Диаграмма состояний

printf("State 1: Waiting " title="9 Фрагмент текстового описания модели на языке Promela inline A0() { stateA0=0; do ::(stateA0==0)-> printf("State 0: Waiting for activation\n"); if ::stateA0=1; lastEvent=10; printf("Going to state 1\n"); fi ::(stateA0==1)-> printf("State 1: Waiting " class="link_thumb"> 9 9 Фрагмент текстового описания модели на языке Promela inline A0() { stateA0=0; do ::(stateA0==0)-> printf("State 0: Waiting for activation\n"); if ::stateA0=1; lastEvent=10; printf("Going to state 1\n"); fi ::(stateA0==1)-> printf("State 1: Waiting for persistent data loading start\n"); if ::stateA0=2; lastEvent=11; printf("Going to state 2\n"); ::stateA0=5; lastEvent=30; printf("Going to state 5\n"); fi... od } proctype Model() { A0(); } init { run Model(); } printf("State 1: Waiting "> printf("State 1: Waiting for persistent data loading start\n"); if ::stateA0=2; lastEvent=11; printf("Going to state 2\n"); ::stateA0=5; lastEvent=30; printf("Going to state 5\n"); fi... od } proctype Model() { A0(); } init { run Model(); }"> printf("State 1: Waiting " title="9 Фрагмент текстового описания модели на языке Promela inline A0() { stateA0=0; do ::(stateA0==0)-> printf("State 0: Waiting for activation\n"); if ::stateA0=1; lastEvent=10; printf("Going to state 1\n"); fi ::(stateA0==1)-> printf("State 1: Waiting ">

10 10 Требования к программе для задачи начальной загрузки

11 11 Отчет программы-верификатора (ошибок не обнаружено) warning: never claim + accept labels requires -a flag to fully verify hint: this search is more efficient if pan.c is compiled -DSAFETY warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) (Spin Version September 2009) + Partial Order Reduction Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles - (not selected) invalid end states - (disabled by never claim) State-vector 28 byte, depth reached 85, errors: states, stored 110 states, matched 228 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) memory usage (Mbyte)

12 12 Фрагмент диаграммы с внесенной ошибкой x10 заменяем на x11

13 13 Отчет программы-верификатора (обнаружена ошибка ) warning: never claim + accept labels requires -a flag to fully verify hint: this search is more efficient if pan.c is compiled -DSAFETY warning: for p.o. reduction to be valid the never claim must be stutter- invariant (never claims generated from LTL formulae are stutter-invariant) pan: claim violated! (at depth 15) pan: wrote SWC1.trail (Spin Version September 2009) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles - (not selected) invalid end states - (disabled by never claim) State-vector 28 byte, depth reached 15, errors: 1 8 states, stored 0 states, matched 8 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) memory usage (Mbyte)

14 14 Вывод контрпримера верификатором SPIN Never claim moves to line 13 [(1)] State 0: Waiting for activation Never claim moves to line 11 [(((lastEvent>10)&&(stateA0==1)))] Going to state 1 Never claim moves to line 21 [(1)] spin: trail ends after 15 steps #processes: 2 stateA0 = 1 lastEvent = 11 15: proc 1 (Model) line 27 "SWC1" (state 65) 15: proc 0 (:init:) line 133 "SWC1" (state 2) 15: proc - (:never:) line 22 "SWC1" (state 16) 2 processes created

15 15 Где еще ведутся аналогичные работы СПбГУ ИТМО (Научно-технический вестник СПбГУ ИТМО. Автоматное программирование. Выпуск ) Ярославский государственный университет им. П.Г. Демидова (Кузьмин Е.В., Соколов В.А. Моделирование, спецификация и верификация «автоматных» программ //Программирование , с ) NASA (NASA: Миссия надежна //Открытые системы )

16 16 Выводы автоматическое построение модели для верификации; точное определение проверяемых свойств с помощью формул темпоральной логики; возможность верифицировать автоматные модели уже на стадии проектирования ПО; использование широко распространенных программ- верификаторов; для автоматных программ удается резко повысить уровень автоматизации их верификации.

17 17 Спасибо за внимание