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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Верификация программ на моделях Лекция №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)завершение•  Не увеличивает пространство достижимых состояний, •  Не увеличивает количество переходов.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций