Лекция 4. Система верификации SPIN. Описание моделей на языке Promela (1158557)
Текст из файла
Верификация программ на моделях Лекция №4 Среда верификации SPIN. Описание моделей на языке Promela. Константин Савенков (лектор) План лекции • Применение SPIN для верификации программ на моделях, • Описание моделей программ на языке Promela: – основные операторы, – недетерминизм, – синхронизация процессов, – задание потока управления модели. Верификация программы при помощи модели • Нам нужно задавать как система устроена и как она должна быть устроена; • Таким образом, нужны две нотации: – чтобы описать поведение (устройство системы), – чтобы описать требования (свойства правильности); • Программа-‐верификатор проверяет, что устройство системы удовлетворяет свойствам правильности; • Выбранная нотация гарантирует разрешимость проверки любого свойства любой модели.
Верификация программы при помощи модели должно быть пусто Возможное поведение программы правильное неправильное SPIN, Promela, LTL • SPIN – Simple Promela INterpreter, • Promela – Process Meta Language, • LTL – Linear Temporal Logic. h]p://spinroot.com документация, дистрибутивы, учебные курсы SPIN, Promela, LTL • SPIN: – моделирование, – верификация; • Promela: – недетерминированный язык с охраняемыми командами, – задача языка – не предотвратить описание моделей плохих программ, – задача языка – разрешить описывать такие модели, которые могут быть верифицированы Процесс верификации Модель на Promela -‐a SPIN свойство правиль-‐ ности -‐i pan.c верифи-‐ цирующий код на С Компи-‐ лятор С испол-‐ няемый верифи-‐ катор -‐v случайное моделирование интерактивное моделирование управляемое моделирование -‐t контр-‐ примеры Ключевые моменты • У моделей – конечное число состояний (потенциально бесконечные элементы моделей в Promela ограничены) – гарантирует разрешимость верификации, – тем не менее, у модели может быть бесконечное число вычислений; • асинхронное выполнение процессов – нет глобальных часов, – по умолчанию синхронизация разных процессов отсутствует; Ключевые моменты • Недетерминированный поток управления – абстракция от деталей реализации; • Понятие выполнимости оператора – с любым оператором связаны понятия предусловия и эффекта, – оператор выполняется (производя эффект), только если предусловие истинно, в противном случае он заблокирован, – Пример: q?m – если канал q не пуст, читаем из него сообщение, иначе ждём.
Устройство модели на Promela Три типа объектов: – процессы, – глобальные и локальные объекты данных, – каналы сообщений. глобаль-‐ ные дан-‐ ные процесс 0 процесс 1 каналы сообщений локаль-‐ ные дан-‐ ные локаль-‐ ные дан-‐ ные Hello, world! немедленное инстанцирование описываем тип процесса active proctype main(){printf(“Hello, world!\n”)}Имя процесса (не ключевое слово) “;” -‐-‐ разделитель команд, а не терминальный символ расширение – опционально Да, это очень похоже на С >spin hello.pmlHello, world!1 process createdHello, world! • Основная структурная единица языка Promela – не функция, а процесс. • Если процесс один, то можно описать его проще: init {printf(“Hello, world!\n”)}не выделяем определение типа процесса • Полная форма – с явным инстанцированием: init {run main()}создаём процесс в ходе выполнения модели Процессы в Promela • Поведение процесса задаётся в объявлении типа процесса (proctype), • Экземпляр процесса – инстанцирование proctype, • Два вида инстанцирования процессов: – в начальном состоянии системы, префикс active– в произвольном достижимом состоянии системы.
оператор runПроцессы в Promela active [2] proctype eager(){run eager();run eager()run eager()run eager()}Два процесса инстанцированы в начальном состоянии системы stopКаждый процесс инстанцирует две своих копии, а затем завершает выполнение Процессы в Promela active [2] proctype eager(){1run eager();run eager()3245}67• Почему такая модель остаётся конечной? – run – оператор-‐выражение, – run либо возвращает pid нового процесса, либо 0, если инстанцирование не удалось, – выражение выполняется, только если возвращает не 0, – максимальное число процессов ограничено 255. Оператор run proctype irun(byte x)предопределённая переменная _pid {printf(“it is me %d, %d\n”,x,_pid)}init{pid a,b;a = run irun(1);b = run irun(2);printf(“I created %d and %d”, a, b)Присваивания и prinƒ выполняются всегда.
Выражения – только если их значение не равно 0. }>spin irun.pmlit is me 1, 1I created 1 and 2it is me 2, 23 processes created>Отступ по умолчанию pid+1 позиция табуляции 1 из 6 возможных чередований Взаимодействие процессов • Два способа синхронизации процессов: – глобальные (разделяемые) переменные, – обмен сообщениями (буферизованные или синхронные каналы), – глобальных часов нет; • У каждого процесса есть локальное состояние: – «счётчик команд» (состояние потока управления), – значения локальных переменных; • У модели в целом – глобальное состояние: – значение глобальных переменных, – содержимое каналов сообщений, – множество активных процессов. Почему число состояний модели конечно? • Число активных процессов конечно, • У каждого процесса – ограниченное число операторов, • Диапазоны типов данных ограничены, • Размер всех каналов сообщений ограничен.
Явная синхронизация процессов bool toggle = true;short cnt;active proctype A() provided (toggle == true){L:cnt++;./spin provided.pml | moreA: cnt=1B: cnt=0A: cnt=1B: cnt=0…printf("A: cnt=%d\n", cnt);toggle = false;goto L}active proctype B() provided (toggle == false){L:cnt--;printf("B: cnt=%d\n", cnt);toggle = true;goto L}Процесс выполняется, только если значение provided clause равно true. По умолчанию значение равно true. Основные операторы Promela • Задают элементарные преобразования состояний, • Размечают дуги в системе переходов соответствующего процесса, • Их немного – всего 6 типов, • Оператор может быть: – выполнимым: может быть выполнен, – заблокированным: (пока что) не может быть выполнен. выполнимость может зависеть от глобального состояния Основные операторы Promela • 3 типа операторов уже встречались: – оператор печати (printf), – оператор присваивания, всегда безусловно выполним, на состояние не влияет всегда безусловно выполним, меняет значение только одной переменной, расположенной слева от «=» – оператор-‐выражение.
выполним, только если выражение не равно 0 (истинно) 2 < 3 – выполним всегда, x < 27 – выполним, только если значение x < 27, 3 + x – выполним, только если x != -‐3. Чередование операторов (интерливинг) • процессы выполняются параллельно и асинхронно, между выполнением двух последовательных операторов одного процесса может быть сколь угодно длинная пауза • произвольная диспетчеризация процессов, • выполнение операторов разных процессов происходит в произвольном порядке, основные операторы выполняются атомарно • в теле одного процесса допускается недетерминированное ветвление.
Два уровня недетерминизма • Внутренний (выбор действия в процессе), Чередование (интерливинг) • Внешний (выбор процесса). a1 a1 a2 b1 b2 a2 b1 b1 a1 b1 a2 b2 b2 a1 b2 a2 Выполнимость операторов • Основной инструмент управления выполнимостью операторов в Promela – выражения (expressions) C while (x <= y)/* wait*/;y++;Promela (x > y) -> y = y + 1;Псевдо-‐операторы • Несколько специфических операторов: – skip: всегда выполним, без эффекта, эквивалент выражения (1), – true: всегда выполним, без эффекта, эквивалент выражения (1), – run: 0, если при создании процесса превышен лимит, _pid в противном случае.
И ещё один тип оператора • assert (выражение) – всегда выполним, не влияет на состояние системы, – SPIN сообщает об ошибке, если значение выражения равно 0 (false), – используется для проверки свойств безопасности (состояний). int n;active proctype invariant() {assert(n <= 3)}В силу асинхронности выполнения процессов, данный оператор может быть выполнен в любой момент. Пример int x;proctype A()значение по умолчанию – 0 {int y = 1;skip;выполнимо, если получится создать процесс B run B();x = 2;(x > 2 && y == 1);printf(“x %d, y %d\n”, x, y)}будет выполнено, только если другой процесс изменит значение x Оператор run • Все выражения без run в Promela не приводят к побочному эффекту; • в отличие от С, в выражении Promela нельзя изменить значение переменной; • в выражении может быть только один оператор run: – run B() && run A() – может быть заблокирован с частичным эффектом, – !(run B()) – эквивалент (_nr_pr >= 255), – run B() && (a>b) – создаёт процессы до тех пор, пока (a <= b); • возврат 0 – как правило, ошибка при разработке модели.
Пример – два процесса mtype = { P, C };перечислимый тип (нумерация с 1) mtype turn = P;active proctype producer(){глобальная переменная по умолчанию – 0, поэтому инициализируем do:: (turn == P) ->бесконечный цикл printf(“Produce\n”);turn = Cod}последовательность вариантов (op“on sequence) active proctype consumer()индикатор начала последовательности {do:: (turn == C) ->printf(“Consume\n”);turn = Pod}страж (guard) Пример – два процесса mtype = { P, C };mtype turn = P;active proctype producer(){-uN – ограничение количества шагов do:: (turn == P) ->printf(“Produce\n”);turn = Cod}active proctype consumer(){do:: (turn == C) ->printf(“Consume\n”);turn = Pod}./spin -u14 pc.pmlProduceConsumeProduceConsume------------depth-limit (-u14 steps) reached#processes: 2turn = C14: proc 1 (consumer) line 17"pc.pml" (state 3)14: proc 0 (producer) line6"pc.pml" (state 4)2 processes createdifactive proctype consumer()active proctype consumer(){{doagain: if:: (turn == C) ->:: (turn == C) ->printf(“Consume\n”);printf(“Consume\n”);turn = Pturn = Pfi;odgoto again}}• break – выход из тела do, • :: else – если ни одна из альтернатив не выполняется, • если выполняется несколько альтернатив – внутренний недетерминизм wait: if:: (turn == P) -> ...:: else -> goto waitfi(turn == P) ->...или (turn == P);...Пример: взаимное исключение bool busy;byte mutex;proctype P(bit i){ (!busy) -> busy = true;Показывает, что критическая секция занята Количество процессов в критической секции mutex++;printf(P%d in critical section\n”,i);mutex--;Ждём, пока критическая секция не освободится, и занимаем её busy = false}active proctype invariant(){ assert(mutex <= 1)потенциальная гонка: оба процесса могут вычислить (!busy) до выполнения оператора busy = true }init {Цикл не нужен atomic { run P(0); run P(1)}}Атомарный запуск двух экземпляров P Запуск верификатора > ./spin -a mutex.pml> gcc -DSAFETY -o pan pan.c> ./panpan: assertion violated (mutex<=1) (at depth 10)pan: wrote mutex.pml.trail(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completed+ Partial Order ReductionFull statespace search for:never claim- (none specified)assertion violations+cycle checks- (disabled by -DSAFETY)invalid end states+State-vector 24 byte, depth reached 19, errors: 173 states, stored32 states, matched105 transitions (= stored+matched)1 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)pan: elapsed time 0 secondsМоделирование контрпримера ./spin -t -p mutex.pmlStarting invariant with pid 0Starting :init: with pid 1Starting P with pid 21:proc 1 (:init:) line 14 "mutex.pml" (state 1) [(run P(0))]Starting P with pid 32:proc 1 (:init:) line 14 "mutex.pml" (state 2) [(run P(1))]3:proc 3 (P) line4 "mutex.pml" (state 1) [(!(busy))]4:proc 2 (P) line4 "mutex.pml" (state 1) [(!(busy))]5:proc 3 (P) line4 "mutex.pml" (state 2) [busy = 1]6:proc 3 (P) line5 "mutex.pml" (state 3) [mutex = (mutex+1)]P1 in critical section7:proc 3 (P) line6 "mutex.pml" (state 4) [printf('P%d in critical section\\n',i)]8:proc 2 (P) line4 "mutex.pml" (state 2) [busy = 1]9:proc 2 (P) line5 "mutex.pml" (state 3) [mutex = (mutex+1)]P0 in critical section10:proc 2 (P) line6 "mutex.pml" (state 4) [printf('P%d in critical section\\n',i)]spin: line 11 "mutex.pml", Error: assertion violatedspin: text of failed assertion: assert((mutex<=1))11:proc 0 (invariant) line 11 "mutex.pml" (state 1) [assert((mutex<=1))]spin: trail ends after 11 steps#processes: 4busy = 1mutex = 211:proc 3 (P) line7 "mutex.pml" (state 5)11:proc 2 (P) line7 "mutex.pml" (state 5)11:proc 1 (:init:) line 15 "mutex.pml" (state 4) <valid end state>11:proc 0 (invariant) line 12 "mutex.pml" (state 2) <valid end state>4 processes createdВзаимное исключение (другой вариант) bit x,y;byte mutex;Сигнал о входе/выходе из критичесой секции active proctype A(){x = 1;(y == 0) ->mutex++;printf("%d\n", _pid);mutex--;x = 0;}Число процессов в критической секции active proctype invariant(){ assert(mutex != 2)}active proctype B(){y = 1;(x == 0) ->mutex++;printf("%d\n",_pid);mutex--;y = 0}!(y == 0) означает, что B – в критической секции Верификация > ./spin -a mutex2.pml> gcc -DSAFETY -o pan pan.c> ./panpan: invalid end state (at depth 3)pan: wrote mutex2.pml.trail(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completed+ Partial Order ReductionFull statespace search for:never claimassertion violationscycle checksinvalid end states- (none specified)+- (disabled by -DSAFETY)+State-vector 20 byte, depth reached 16, errors: 123 states, stored3 states, matched26 transitions (= stored+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)pan: elapsed time 0 secondsВзаимное исключение (другой вариант) bit x,y;byte mutex;active proctype A(){x = 1;(y == 0) ->mutex++;printf("%d\n", _pid);mutex--;x = 0;}active proctype invariant(){ assert(mutex != 2)}active proctype B(){y = 1;(x == 0) ->mutex++;printf("%d\n",_pid);mutex--;y = 0}гонка если эти операторы будут выполнены последовательно, процессы заблокируют друг друга (deadlock, invalid endstate) Моделирование контрпримера > ./spin -t -p mutex2.pmlStarting A with pid 0Starting B with pid 1Starting invariant with pid 21:proc 2 (invariant) line 25 "mutex2.pml" (state 1)[assert((mutex!=2))]2: proc 2 terminates3:proc 1 (B) line 16 "mutex2.pml" (state 1)[y = 1]4:proc 0 (A) line6 "mutex2.pml" (state 1)[x = 1]spin: trail ends after 4 steps#processes: 2x = 1y = 1mutex = 04:proc 1 (B) line 17 "mutex2.pml" (state 2)4:proc 0 (A) line7 "mutex2.pml" (state 2)3 processes created>Алгоритм Петерсона (1981) mtype = {A_Turn, B_Turn};bool x,y;byte mutex;mtype turn = A_Turn;active proctype A(){ x = true;turn = B_Turn;(!y || turn == A_Turn) ->mutex++;/*critical section*/mutex--;x = false;}active proctype invariant(){ assert(mutex <= 1)}Сигнал о входе/выходе из критичесой секции Число процессов в критической секции Чей ход? active proctype B(){ y = true;turn = A_Turn;(!x || turn == B_Turn) ->mutex++;/*critical section*/mutex--;y = false;}Вариант алгоритма Лампорта (1981) Чей ход? byte turn[2];byte mutex;active [2] proctype P(){ bit i = _pid;L:turn[i] = 1;turn[i] = turn[i+1];(turn[1-i] == 0) ||(turn[i] < turn[1-i]) ->mutex++;assert(mutex == 1);mutex--;turn[i] = 0;goto L;}Число процессов в критической секции Может ли алгоритм достичь максимального i = 255? Будет ли алгоритм корректен, если при достижении 255 обнулять i? Основные операторы языка Promela • присваивание:• выражение: • печать: x++, x--, x = x + 1,x = run P(); (x), (1), run P(),skip, true, else, timeout;printf(“x = %d\n”, x); • ассерт:assert(1+1 == 2),assert(false); • отправка сообщения: q!m; • приём сообщения:q?m; Последние два типа операторов Promela отправка и приём сообщений s2r sender receiver r2s s2r!msgs2r?msgr2s!ackr2s?ack! – отправка, ? -‐ приём Каналы сообщений • Сообщения передаются через каналы (очереди/буфера ограниченного объёма), • каналы бывают двух типов: – буферизованные (асинхронные), – небуферизованные (синхронные, рандеву); Каналы сообщений • пример объявления канала: имя типа имя переменной инициализация chan x = [10] of {int, short, bit};максимальное число сообщений в канале; 0 задаёт рандеву структура пересылаемых сообщений (список имён типов полей сообщения) Каналы сообщений • пример объявления канала: неинициализированная канальная переменная a chanchanchanchanканал c типа «рандеву» a;c = [0] of {bit};toR = [2] of {mtype, bit, chan};line[2] = [1] of {mtype, record};массив из двух каналов пользовательский тип каналы можно передавать по каналам Объявление mtype (mtype = message type) • способ определить символьные константы (до 255), • объявление mtype: в итоге объявляется 6 констант mtype = {foo, bar};mtype = {ack, msg, err, interrupt};• объявление переменных типа mtype: неинициализированная, значение 0 mtype a;mtype b = foo;значение всегда отлично от 0 Отправка и приём сообщений • отправка: ch!expr1,...,exprn– значения expri должны соответствовать типам в объявлении канала; – выполнима, если заданный канал не полон; • приём: ch?const1 или var1,…,constn или varn– значения vari становятся равны соотв.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
