lect06 (1158547)

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

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

Верификация программна моделяхЛекция №6Свойства линейного времени.Спецификация и верификация свойств припомощи Spin.Константин Савенков (лектор)План лекции• Рассуждения о правильности программы,• Свойства безопасности и живучести,• Инструменты SPIN/Promela дляспецификации свойств.Верификация программы припомощи моделидолжно бытьпустоВозможное поведениепрограммыправильное неправильноеОсновные компоненты модели в SPIN• Спецификация поведения (возможное поведение)– асинхронное выполнение процессов,– переменные, типы данных,– каналы сообщений;• Свойства правильности (правильное поведение)–––––ассерты,метки завершения и прогресса,утверждения о невозможности (never claims),трассовые ассерты,свойства по умолчанию:– отсутствие тупика,– отсутствие недостижимого кода,– формулы темпоральной логики.Рассуждения о правильностипрограммы• Требования правильности задаются как утверждения овозможных или невозможных вариантах выполнениямодели,– рассуждения о вероятности не допускаются из соображенийстрогости доказательства;• Мы утверждает, что некоторые варианты выполнениямодели– либо невозможны,– либо неизбежны;• Двойственность утверждений:– если что-то неизбежно, то противоположное – невозможно,– если что-то невозможно, то противоположное – неизбежно,– используя логику, можно переходить от одного к другому припомощи логического отрицания.Свойства безопасности и живучести(автор – Leslie Lamport)безопасностьживучесть• «ничего плохого никогда непроизойдёт»;• «рано или позднопроизойдёт что-то хорошее»;• пример: инвариант системы• пример: «отзывчивость»– (х всегда меньше y);• задача верификатора – найтивычисления, которые ведут кнарушению свойствабезопасности (то «плохое»,которое никогда не должнопроизойти)– если отправлен запрос, торано или поздно будетсгенерирован ответ;• задача верификатора – найтивычисления, в которых это«хорошее» можетоткладываться добесконечностиНемного подробнее…• Свойства безопасности – самые простыесвойства («состояние, где истинно φ,недостижимо»).• Можно ли в рамках свойства безопасностисформулировать, что φ неизбежно?• «состояние, где истинно !φ, недостижимо»– не то, это слишком сильное свойство;• «состояние, где истинно φ, достижимо»– а это, наоборот, слишком слабое.Немного подробнее…• «φ неизбежно» – означает, что φобязательно достижима;• для спецификации такой модальности инужны свойства живучести.Способы описания свойствправильности• Свойства правильности могут задаваться как:– свойства достижимых состояний (свойствабезопасности),– свойства последовательностей состояний (свойстваживучести);• В языке 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 получает доступк критической секции, т.е.

когдапроцесс semaphore достигаетсостояния s1.Теперь верификатор будет искатьдостижимые циклы бездействия.Примерbyte x = 2;active proctype A(){do:: x = 3 - xod}• x бесконечно варьирует между 2 и 1,• у каждого процесса – одно состояние,• метки progress не используются => поумолчанию всякий цикл рассматриваетсякак потенциально бездейственный>spin -a fair.pml>gcc -DNP -o pan pan.cactive proctype B() >./pan -l{Обнаружение цикловpan: non-progress cycle (at depth 2)dopan: wrote fair.pml.trailбездействия:: x = 3 - x(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completedod+ Partial Order Reduction}Full statespace search for:Запуск алгоритмаnever claim+assertion violations+ (if within проверкиscope of claim)non-progress cycles+ (fairness disabled)Q1: Что будет, еслиinvalid end states- (disabled by never claim)State-vector 24 byte, depth reached 5, errors: 1отметить один из do-od3 states, storedциклов меткой progress?0 states, matchedQ2: А если разметить3 transitions (= stored+matched)0 atomic stepsоба цикла?hash conflicts:0 (resolved)2.501memory usage (Mbyte)Какой цикл мы обнаружили?>spin -t -p fair.pmlStarting A with pid 0Starting B with pid 1spin: couldn't find claim (ignored)2:proc 1 (B) line 13 "fair.pml"<<<<<START OF CYCLE>>>>>4:proc 1 (B) line 13 "fair.pml"6:proc 1 (B) line 13 "fair.pml"spin: trail ends after 6 steps#processes: 2x = 16:proc 1 (B) line 12 "fair.pml"6:proc 0 (A) line5 "fair.pml"2 processes created(state 1)[x = (3-x)](state 1)(state 1)[x = (3-x)][x = (3-x)](state 2)(state 2)Мы не знаем относительно скорости выполненияпроцессов:• возможно, что процесс B выполнит бесконечно больше шагов,чем процесс A;• цикл бездействия, обнаруженный Spin – это не обязательносправедливый цикл.Справедливые циклы• Часто мы ожидаем конечного прогресса:– если процесс может сделать шаг, он в конце концов егосделает.• Существует два основных варианта справедливости:1) слабая справедливость:– если оператор выполним бесконечно долго, то он вконце концов будет выполнен;2) сильная справедливость:– если оператор выполним бесконечно часто, то он вконце концов будет выполнен.• Справедливость применима как к внешнему, так и квнутреннему недетерминизму.выбор оператораvs.

выбор процессаbyte x = 2, y = 2;active proctype A(){do:: x = 3 – x;:: y = 3 - yod}active proctype B(){do:: x = 3 – x;:: y = 3 - yod}x = 3-xx = 3-xABy = 3-yy = 3-yy = 3-yx = 3-xAx = 3-xy = 3-ySPIN поддерживает один из вариантов слабойсправедливости (>pan -f):«если процесс содержит хотя бы один оператор,который бесконечно долго остаётся выполнимым,то этот процесс рано или поздно сделает шаг».Это касается только потенциально бесконечных вычислений(циклов).Поиск слабо справедливыхциклов бездействия>./pan -l -fpan: non-progress cycle (at depth 6)pan: wrote fair.pml.trail>./spin -t -p fair.pmlStarting A with pid 0Starting B with pid 1spin: couldn't find claim (ignored)2:proc 1 (B) line 13 "fair.pml"4:proc 1 (B) line 13 "fair.pml"6:proc 0 (A) line6 "fair.pml"<<<<<START OF CYCLE>>>>>8:proc 1 (B) line 13 "fair.pml"10:proc 0 (A) line6 "fair.pml"spin: trail ends after 10 steps#processes: 2x = 110:proc 1 (B) line 12 "fair.pml"10:proc 0 (A) line5 "fair.pml"2 processescreatedТеперьв цикле естьшагиобоих процессов(state 1)(state 1)(state 1)[x = (3-x)][x = (3-x)][x = (3-x)](state 1)(state 1)[x = (3-x)][x = (3-x)](state 2)(state 2)Указываем полезные действияbyte x = 2, y = 2;active proctype A(){do:: x = 3 – x;:: y = 3 – y; progress: skipod}ВОПРОСЫ:active proctype B(){do:: x = 3 – x;:: y = 3 – y; progress: skipod}• А справедливые циклы?• Будут ли циклы бездействияс меткой progress в одномпроцессе?• А если метки есть в обоихпроцессах?Использование условийсправедливости• Любой тип справедливости можно описатьпри помощи формулы LTL (позже)• добавление предположения осправедливости всегда увеличиваетсложность верификации• использование сильной справедливостисущественно дороже слабой:– слабая: сложность (по времени и памяти) растётлинейно от числа активных процессов,– сильная: сложность растёт квадратично.Пример: протокол голосования#define N#define I#define L5 /* nr of processes (use 5 for demos)*/3 /* node given the smallest number*/10 /* size of buffer (>= 2*N) *//* file ex.8 */mtype = { one, two, winner };chan q[N] = [L] of { mtype, byte};byte nr_leaders = 0;proctype node (chan in, out; byte mynumber){bit Active = 1, know_winner = 0;byte nr, maximum = mynumber, neighbourR;...}init {byte proc;atomic {proc = 1;do:: proc <= N ->run node (q[proc-1], q[proc%N],(N+I-proc)%N+1);proc++:: proc > N ->breakod}}out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr)fi:: in?winner,nr;if:: nr != mynumber:: else -> nr_leaders++;fi;if:: know_winner:: else -> out!winner,nrfi;breakodЗапускаем моделирование>spin -cproc 0 =proc 1 =proc 2 =proc 3 =proc 4 =proc 5 =q\p05.3.2.4.2.4.1.3.1.5.2.1.5.3.5.4.1.4.leader.pml:init:nodenodenodenodenode12345...out!one,5.out!one,2out!one,3..out!one,1.in?one,3...in?one,1....out!one,4..in?one,2in?one,4....in?one,5out!two,4....out!two,5...out!two,1.out!two,3....in?two,1..out!two,2in?two,5...in?two,21.....out!one,53...in?two,32..in?two,41.in?one,52.out!one,52..in?one,53..out!one,53...in?one,54...out!one,54....in?one,55....out!one,55.....in?one,51.....out!winner,51.in?winner,52.out!winner,52..in?winner,53..out!winner,53...in?winner,54...out!winner,54....in?winner,55....out!winner,55.....in?winner,5------------final state:------------6 processes createdВерификация по умолчанию>./spin -a leader.pml>./gcc -o pan pan.c>./pan(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+State-vector 200 byte, depth reached 106, errors: 04813 states, stored1824 states, matched6637 transitions (= stored+matched)12 atomic stepshash conflicts:13 (resolved)Stats on memory usage (in Megabytes):0.991equivalent memory usage for states (stored*(State-vector + overhead))1.070actual memory usage for states (unsuccessful compression: 107.92%)state-vector as stored = 217 byte + 16 byte overhead2.000memory used for hash table (-w19)0.305memory used for DFS stack (-m10000)Ошибок нет, но мы ещё3.282total actual memory usageunreached in proctype nodeне сказали, что долженline 40, state 26, "out!two,nr"делать алгоритм(1 of 44 states)unreached in proctype :init:(0 of 11 states)pan: elapsed time 0.03 secondsПохоже, в модели естьpan: rate 160433.33 states/secondнедостижимый кодСвойстваправильности• При помощиассертов можнопроверить двапростых факта:– должен выигратьпроцесс смаксимальнымномером,– должен быть толькоодин победитель.• Правда ли операторотправки сообщениянедостижим?out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr); assert(false)fi:: in?winner,nr -> assert(nr == N) ;if:: nr != mynumber:: else -> nr_leaders++; assert(nr_leaders == 1)fi;if:: know_winner:: else -> out!winner,nrfi;breakodБолее осмысленная верификация>./spin -a leader.pml>./gcc -DSAFETY -o pan pan.c>./pan(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claimassertion violationscycle checksDSAFETY)invalid end states- (none specified)+- (disabled by -memory usage (Mbyte)unreached in proctype nodeline 40, state 26, "out!two,nr"line 40, state 27, "assert(0)"(2 of 47 states)unreached in proctype :init:(0 of 11 states)pan: elapsed time 0.01 secondsПоявились ассерты+State-vector 196 byte, depth reached 112, errors: 04819 states, stored1824 states, matched6643 transitions (= stored+matched)12 atomic stepshash conflicts:5 (resolved)3.379Проверяем простейшиесвойства безопасностиОшибок не найдено!Число состоянийувеличилось: ассертыДействительно,недостижимое состояниеAlternating Bit Protocol(с потерей сообщения и таймаутом)mtype = {msg, ack};chan to_s = [1] of {mtype, bit};chan to_r = [1] of {mtype, bit};chan from_s = [1] of {mtype, bit};chan from_r = [1] of {mtype, bit};active proctype sender(){ bit a;do:: from_s!msg,a ->if:: to_s?ack,eval(a) ->a = 1 - a:: timeoutfiod}active proctype receiver(){ bit a;do:: to_r?msg,eval(a) ->from_r!ack,a;progress:a = 1 - aod}active proctype channel(){ mtype m; bit a;do:: from_s?m,a ->if:: to_r!m,a:: skipfi:: from_r?m,a ->to_s!m,aod}Теряем сообщениеПовторная отправкаБудет ли алгоритм эффективноработать при потере сообщений?Проверяем!> ./spin -a abp_lossy.pml> gcc -DNP -o pan pan.c> ./pan -lpan: non-progress cycle (at depth 4)pan: wrote abp_lossy.pml.trailХорошо бырассмотретьи другиесценарии!В найденном сценарии мыбесконечно часто теряемсообщение./spin -t -c abp_lossy.pmlproc 0 = senderproc 1 = receiverproc 2 = channelspin: couldn't find claim (ignored)q\p011from_s!msg,01..from_s?msg,0<<<<<START OF CYCLE>>>>>1from_s!msg,01..from_s?msg,0spin: trail ends after 12 steps------------final state:------------#processes: 3queue 1 (from_s):12:proc 2 (channel) line 33 "abp_lossy.pml" (state 4)12:proc 1 (receiver) line 21 "abp_lossy.pml" (state 4)12:proc 0 (sender) line 11 "abp_lossy.pml" (state 5)3 processes createdУточняем свойствоactive proctype channel(){ mtype m; bit a;do:: from_s?m,a ->if:: to_r!m,a:: skip; progress: skipfi:: from_r?m,a ->to_s!m,aod}active proctype receiver(){ bit a;do:: to_r?msg,eval(a) ->from_r!ack,a;progress:a = 1 - aod}Размечаем циклпотери сообщенийметкой прогресса,исключая из поискаУточнённая проверка> ./spin -a abp_lossy2.pml> gcc -DNP -o pan pan.c> ./pan -l(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claim+assertion violations+ (if within scope of claim)non-progress cycles+ (fairness disabled)invalid end states- (disabled by never claim)State-vector 60 byte, depth reached 53, errors: 073 states, stored (98 visited)64 states, matched162 transitions (= visited+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)unreached in proctype senderline 17, state 10, "-end-"(1 of 10 states)unreached in proctype receiverline 27, state 7, "-end-"(1 of 7 states)unreached in proctype channelline 40, state 12, "-end-"(1 of 12 states)Единственныйциклбездействиясвязан сбесконечнойпотерейсообщенийПример: протокол голосования#define N#define I#define L5 /* nr of processes (use 5 for demos)*/3 /* node given the smallest number*/10 /* size of buffer (>= 2*N) *//* file ex.8 */mtype = { one, two, winner };chan q[N] = [L] of { mtype, byte};byte nr_leaders = 0;proctype node (chan in, out; byte mynumber){bit Active = 1, know_winner = 0;byte nr, maximum = mynumber, neighbourR;...}init {byte proc;atomic {proc = 1;do:: proc <= N ->run node (q[proc-1], q[proc%N],(N+I-proc)%N+1);proc++:: proc > N ->breakod}}out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr)fi:: in?winner,nr;if:: nr != mynumber:: else -> nr_leaders++;fi;if:: know_winner:: else -> out!winner,nrfi;breakodСвойстваправильности• Кое-что мы ужепроверили припомощи ассертов:1.

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

Тип файла PDF

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

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

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