Лекция 5. Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin (К. Савенков - Верификация программ на моделях (2012))

Верификация  программ  на  моделях  Лекция  №5  Практические  приёмы  абстракции.  Свойства  линейного  времени.  Спецификация  и  верификация  свойств  при  помощи  Spin.  Константин  Савенков  (лектор)  План  лекции  • • • • Практические  приёмы  абстракции,  Рассуждения  о  правильности  программы,  Свойства  безопасности  и  живучести,  Инструменты  SPIN/Promela  для  спецификации  свойств.  Практические  приёмы  абстракции  Общая  схема  Программа  на  С  Модель  на  Promela  •  Неправильный  подход!  –  Если  строить  модель  без  оглядки  на  проверяемые  свойства,  то  она  получится  слишком  детальной.

 –  Скорее  всего,  не  хватит  ресурсов  на  верификацию.    Общая  схема  Программа  на  С  Модель  на  Promela  Проверяемые  свойства  •  Модель  должна  моделировать  только  то,  что  влияет  на  выполнимость  проверяемых  свойств.  Пример  void f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}•  Модель  точная,  но  у  неё  слишком  много  достижимых  состояний.  •  Давайте  посмотрим  на  заданные  свойства.  proctype f(int x){do:: x < 3 ->printf(“Case 1\n”);x = x + 1:: x >= 10 ->break;:: else ->printf(“Case 2\n”);x = x + 1od}init {int x;do:: x++;:: x--;:: break;od;run f(x)}Пример  void f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}«Проверить,  что  перед  печатью  “Case  2”  всегда  была  выполнена  печать  “Case  1”.»  proctype f(int x){do:: x < 3 ->printf(“Case 1\n”);x = x + 1:: x >= 10 ->break;:: else ->printf(“Case 2\n”);x = x + 1od}init {int x;do:: x++;:: x--;:: break;od;run f(x)}Пример  void f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}«Проверить,  что  перед  печатью  “Case  2”  всегда  была  выполнена  печать  “Case  1”.»  mtype {X1, X2, X3};proctype f(mtype x){do:: x == X1 ->printf(“Case 1\n”);incr(x);:: x == X3 ->break;:: x == X2 ->printf(“Case 2\n”);incr(x);inline incr(x){odif}:: x += 1;init{:: skipmtype x;fiif}:: x = X1:: x = X2:: x = X3fi;run f(x)}Не  загромождаем  модель  Приёмы  абстракции  • • • • • Абстракция  предикатов  Абстракция  типов  данных  Абстракция  наблюдаемых  переменных  Абстракция  от  «лишнего»  кода  Абстракция  от  функций  и  системных  вызовов  Абстракция  предикатов  if(x < 0){printf (“Case 1”);}else{printf (“Case 2”);}…if:: printf (“Case 1”);:: printf (“Case 2”);fi•  В  модели  увеличивается  количество  возможных  вычислений  –  если  формула  не  нарушается  ни  на  одном  вычислении  модели,  то  на  исходной  программе  она  также  будет  выполнима,  –  если  формула  нарушается  на  одном  из  «добавленных»  вычислений,  необходимо  увеличить  уровень  детализации  модели  Абстракция  типов  данных  int x;…if(x < 0) {…}else {if(x < 3) {…}else {…}…}mtype { X1, /*x < 0*/X2, /*0 <= x < 3*/X3 /*x >= 3*/};if:: x == X1 -> …:: x == X2 -> …:: x == X3 -> …fi•  Диапазон  типа  данных  разбивается  на  классы  эквивалентности  относительно  конструкций  организации  потока  управления  и  проверяемых  свойств.

 •  Необходимо  корректно  моделировать:  –  предикаты  в  операторах  ветвления,  –  операторы,  изменяющие  значения  переменных  этого  типа.  Абстракция  наблюдаемых  переменных  •  Из  модели  удаляются  переменные,  значения  которых  не  влияют  на  выполнимость  заданных  свойств:  –  не  используются  при  формулировке  свойства,  –  не  влияют  на  поток  управления  модели.  •  Операторы  модели  могут  быть  связаны  достаточно  сложными  зависимостями  по  данным  и  управлению,  поэтому  в  ходе  удаления  переменных  допускается  только  расширение  множества  возможных  вычислений  модели  Абстракция  наблюдаемых  переменных  int x;…while (x != 0){x = get_value();}…printf (“Something\n”);printf (“Something\n”);do:: skip:: breakod;printf(“Something\n”)•  Свойство  –  операция  печати  будет  выполнена  один  раз,  •  Если  абстрагируемся  от  цикла  –  теряем  возможность  бесконечного  зацикливания  (сужаем  множество  возможных  вычислений).

 Абстракция  от  «лишнего»  кода  …some_func();printf(“Func called!\n”)……some_func: skip;…•  Свойство  –  some_func()  будет  вызвана.  •  Можно  абстрагироваться  от:  –  кода,  не  влияющего  на  проверяемое  свойство  (prink),  –  реального  выполнения  операторов,  если  нас  интересует  лишь  факт  его  выполнения  («функция  была  вызвана»).

 •  Здесь  также  необходимо  следить  за  допустимыми  вычислениями.  …int x;x = some_func();if (x)……int x;some_func: skip;if:: x -> ……Абстракция  от  функций  и  системных  вызовов  f  f(){sys_call();}sys_call  call  res  •  Выполнение  реальной  функции  заменяется  на  обмен  сообщениями  с  процессом-­‐«заглушкой»,  •  Обмен  сообщениями  должен  корректно  моделировать  вызов  функции:  –  синхронное  взаимодействие,  гарантированный  отклик.  От  чего  не  стоит  абстрагироваться  •  Поток  управления:  –  ветвление,  циклы;  •  Можно  добавлять  новые  ветви  и  пути  выполнения:  –  см.

 «абстракция  предикатов»,  –  если  на  добавленных  путях  будет  нарушаться  свойство,  то  эта  ошибка  будет  обнаружена  при  анализе  контрпримера.  •  Нельзя  убирать  пути  выполнения  на  основе  «метода  пристального  взгляда»  –  можно  случайно  убрать  путь  выполнения  программы,  на  котором  происходит  нарушение  свойства  правильности  программы.  Пример  поэтапной  абстракции  int x = 0;…while (x < 5){x++;}…printf (“Something\n”);1  cycle: do:: inc: skip:: breakod;printf(“Something\n”)2  //finite cycle removedprintf (“Something\n”);•  Свойство  –  «Рано  или  поздно  “Something”  будет  напечатано».

 •  При  полной  предикатной  абстракции  модель  корректна,  но  не  адекватна  свойству.  •  Если  мы  докажем,  что  в  цикле  –  конечное  число  итераций,  от  него  можно  абстрагироваться.  •  Для  этого  нужно  показать,  что  между  двумя  проверками  условия  цикла  всегда  происходит  инкремент  х.  Типичные  ошибки  и  «странности»  bit b;...if:: b ==:: b ==:: b ==:: b ==fi«Я  хочу  повысить  вероятность  b  ==  1»  1110->->->->AAABНедетерминизм  связан    не  с  понятием  вероятности,  а  с  понятием  возможности  Типичные  ошибки  и  «странности»  bit b;active proctype A(){do:: b == 1 -> A:: else -> skipod}bit b;active proctype A(){(b == 1) -> A}«Я  жду,  пока  не  выполнится  условие!»  Используйте  нативные  конструкции  Promela!  Типичные  ошибки  и  «странности»  bit b;...if:: b = 1:: b = 0fi;if:: b == 1 -> A:: b == 0 -> Bfiif:: A:: Bfi«Переменная  может  принимать  разные  значения»  От  неё  вообще  нужно  абстрагироваться!  Типичные  ошибки  и  «странности»  chan f1 = [0] of bit;chan f2 = [0] of bit;active proctype caller(){do:: if::f1!m;:: else -> breakfi;...od}active proctype callee(){msg m;do:: f1?m -> f2!mod}«Но  я  же  должен  учесть,  что  канал  может  быть  занят!»  Некорректное  моделирование  вызова  функции:  вызов  «сбрасывается»,  если  процесс-­‐«заглушка»  занят  Типичные  ошибки  и  «странности»  «Я  сначала  построю  модель,  а  потом  уберу  всё  лишнее»  Сначала  прочитайте  спецификацию!!!  План  лекции  • • • • Практические  приёмы  абстракции,  Рассуждения  о  правильности  программы,  Свойства  безопасности  и  живучести,  Инструменты  SPIN/Promela  для  спецификации  свойств.

 Верификация  программы  при  помощи  модели  должно  быть  пусто  Возможное  поведение  программы  правильное   неправильное  Основные  компоненты  модели  в  SPIN  •  Спецификация  поведения  (возможное  поведение)  –  асинхронное  выполнение  процессов,  –  переменные,  типы  данных,  –  каналы  сообщений;  •  Свойства  правильности  (правильное  поведение)  –  ассерты,  –  метки  завершения  и  прогресса,  –  утверждения  о  невозможности  (never  claims),  –  трассовые  ассерты,  –  свойства  по  умолчанию:  –  отсутствие  тупика,  –  отсутствие  недостижимого  кода,  –  формулы  темпоральной  логики.  Рассуждения  о  правильности  программы  •  Требования  правильности  задаются  как  утверждения  о  возможных  или  невозможных  вариантах  выполнения  модели,  –  рассуждения  о  вероятности  не  допускаются  из  соображений  строгости  доказательства;  •  Мы  утверждаем,  что  некоторые  варианты  выполнения  модели  –  либо  невозможны,  –  либо  неизбежны;  •  Двойственность  утверждений:  –  если  что-­‐то  неизбежно,  то  противоположное  –  невозможно,  –  если  что-­‐то  невозможно,  то  противоположное  –  неизбежно,  –  используя  логику,  можно  переходить  от  одного  к  другому  при  помощи  логического  отрицания.

 Свойства  безопасности  и  живучести  (автор  –  Leslie  Lamport)  безопасность  живучесть  •  «ничего  плохого  никогда  не  произойдёт»;  •  «рано  или  поздно  произойдёт  что-­‐то  хорошее»;  •  пример:  инвариант  системы  •  пример:  «отзывчивость»  –  (х  всегда  меньше  y);  •  задача  верификатора  –  найти  вычисления,  которые  ведут  к  нарушению  свойства  безопасности  (то  «плохое»,  которое  никогда  не  должно  произойти)  –  если  отправлен  запрос,  то  рано  или  поздно  будет  сгенерирован  ответ;  •  задача  верификатора  –  найти  вычисления,  в  которых  это  «хорошее»  может  откладываться  до  бесконечности  Немного  подробнее…  •  Свойства  безопасности  –  самые  простые  свойства  («состояние,  где  истинно  φ,  недостижимо»).  •  Можно  ли  в  рамках  свойства  безопасности  сформулировать,  что  φ  неизбежно?  •  «состояние,  где  истинно  !φ,  недостижимо»    –  не  то,  это  слишком  сильное  свойство;  •  «состояние,  где  истинно  φ,  достижимо»      –  а  это,  наоборот,  слишком  слабое.

     Немного  подробнее…  •  «φ  неизбежно»  –  означает,  что  φ  обязательно  достижимо;  •  для  спецификации  такой  модальности  и  нужны  свойства  живучести.    План  лекции  • • • • Практические  приёмы  абстракции,  Рассуждения  о  правильности  программы,  Свойства  безопасности  и  живучести,  Инструменты  SPIN/Promela  для  спецификации  свойств.

 Способы  описания  свойств  правильности  •  Свойства  правильности  могут  задаваться  как:  –  свойства  достижимых  состояний  (свойства  безопасности),  –  свойства  последовательностей  состояний  (свойства  живучести);  •  В  языке  Promela  –  ассерты:  •  локальные  ассерты  процессов,  •  инварианты  системы  процессов;  –  метки  терминальных  состояний:  •  задаём  допустимые  точки  останова  процессов;    –  метки  прогресса  (поиск  циклов  бездействия);  –  утверждения  о  невозможности  (never  claims)  •  например,  определяются  LTL-­‐формулами;  –  трассовые  ассерты.  свойства  состояний  свойства    последова-­‐  тельностей    состояний  Ассерты  –  самый  древний  способ  проверить  правильность  программы  byte state = 1;active proctype A(){(state == 1)assert(state}active proctype B(){(state == 1)assert(state}-> state++;== 2)-> state--;== 0)>spin -a simple.pml>gcc -o pan pan.c>./pan -Epan: assertion violated (state==2) (at depth 6)pan: wrote simple.pml.trail...>spin -t -p simple.pmlStarting A with pid 0Starting B with pid 11:proc 1 (B) line7 "simple.pml" (state 1)2:proc 0 (A) line3 "simple.pml" (state 1)3:proc 1 (B) line7 "simple.pml" (state 2)4:proc 1 (B) line8 "simple.pml" (state 3)5: proc 1 terminates6:proc 0 (A) line3 "simple.pml" (state 2)spin: line4 "simple.pml", Error: assertion violated...Игнорируем  ошибки    некорректного    останова  процесса  [((state==1))][((state==1))][state = (state-1)][assert((state==0))][state = (state+1)]Предотвращение  гонки  byte state = 1;active proctype A(){atomic((state == 1) -> state++);assert(state == 2)}active proctype B()>spin -a simple.pml{atomic((state ==1) -o->panstate--);>gccpan.c-Eassert(state ==>./pan0)добавляем  две  атомарные  последовательности  (Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claim- (none specified)assertion violations+acceptancecycles- (not selected)invalid end states- (disabled by -E flag)State-vector 20 byte, depth reached 3, errors: 06 states, stored0 states, matched6 transitions (= stored+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)unreached in proctype A(0 of 5 states)unreached in proctype B(0 of 5 states)Задание  инвариантов  системы  mtype = {p, v};chan sem = [0] of {mtype};byte count;active proctype semaphore(){do:: sem!p ->sem?vod}active proctype user(){do:: sem?p;count++;/*critical section*/count--;sem!vod}active proctype invariant(){assert(count <= 1)}Сколько  «стоит»  такая  проверка?  инстанцированиеassert(count <= 1)завершениеДобавление  такого  инварианта  увеличивает  пространство  поиска    в  3  раза…  (с  16  достижимых  состояний  до  48)  Проявляем  интуицию  mtype = {p, v};chan sem = [0] of {mtype};byte count;active proctype semaphore(){do:: sem!p ->sem?vod}active proctype user(){do:: sem?p;count++;/*critical section*/count--;sem!vod}active proctype invariant(){do ::assert(count <= 1) od}Сколько  «стоит»  такая  проверка?  инстанцированиеassert(count <= 1)Пространство  достижимых  состо-­‐  яний  не  увеличивается,  однако  добавляется  много  новых  переходов  Ещё  лучше…  mtype = {p, v};chan sem = [0] of {mtype};byte count;active proctype semaphore(){do:: sem!p ->sem?vod}active proctype user(){do:: sem?p;count++;/*critical section*/count--;sem!vod}active proctype invariant(){d_step { !(count <= 1) ->assert(count <= 1)}}Сколько  «стоит»  такая  проверка?  инстанцирование(count > 1) ->assert(count <= 1)завершение•     Не  увеличивает  пространство        достижимых  состояний,  •     Не  увеличивает  количество    переходов.