Лекция 4. Система верификации SPIN. Описание моделей на языке Promela (К. Савенков - Верификация программ на моделях (2012))

Верификация  программ  на  моделях  Лекция  №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  становятся  равны  соотв.