6 - Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin (К. Савенков - Презентации лекций)

Верификация программна моделяхЛекция №6Практические приёмы абстракции.Свойства линейного времени. Спецификация иверификация свойств при помощи 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() будет вызвана.• Можно абстрагироваться от:– кода, не влияющего на проверяемое свойство (printf),– реального выполнения операторов, если нас интересует лишьфакт его выполнения («функция была вызвана»).• Здесь также необходимо следить за допустимымивычислениями.…int x;x = some_func();if (x)……int x;some_func: skip;if:: x -> ……Абстракция от функций и системныхвызововff(){sys_call();}sys_callcallres• Выполнение реальной функции заменяется наобмен сообщениями с процессом-«заглушкой»,• Обмен сообщениями должен корректномоделировать вызов функции:– синхронное взаимодействие, гарантированный отклик.От чего не стоит абстрагироваться• Поток управления:– ветвление, циклы;• Можно добавлять новые ветви и пути выполнения:– см.

«абстракция предикатов»,– если на добавленных путях будет нарушаться свойство,то эта ошибка будет обнаружена при анализеконтрпримера.• Нельзя убирать пути выполнения на основе «методапристального взгляда»– можно случайно убрать путь выполнения программы,на котором происходит нарушение свойстваправильности программы.Пример поэтапной абстракцииint x = 0;…while (x < 5){x++;}…printf (“Something\n”);1cycle: 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) line72:proc 0 (A) line33:proc 1 (B) line74:proc 1 (B) line85: proc 1 terminates6:proc 0 (A) line3spin: line4 "simple.pml",..."simple.pml""simple.pml""simple.pml""simple.pml"(state(state(state(state1)1)2)3)"simple.pml" (state 2)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) -> state--);>gcc -o pan pan.cassert(state ==>./pan0)-Eдобавляем две атомарныепоследовательности(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)завершение• Не увеличивает пространстводостижимых состояний,• Не увеличивает количествопереходов.Допустимые состояния остановаmtype = {p, v};semaphoreusers0s0chan sem = [0] of {mtype};byte count;active proctype semaphore(){end:do:: sem!p ->sem?vod}active proctype user(){end:do:: sem?p;count++;/*critical section*/count--;sem!vod}sem!psem?psem?vs1s1count++s2count-s3sem!vНи один из процессов не должензавершаться; допустимое состояниеостанова для обоих процессов – s0.Верификатор должен искатьнедопустимые состояния останова, неотвлекаясь на допустимые.Состояния прогрессаmtype = {p, v};semaphoreusers0s0chan sem = [0] of {mtype};byte count;active proctype semaphore(){do:: sem!p ->progress: sem?vod}active proctype user(){do:: sem?p;count++;/*critical section*/count--;sem!vod}sem!psem?psem?vs1s1count++s2count-s3sem!vСистема демонстрирует прогрессвсякий раз, когда user получает доступк критической секции, т.е.