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

 зачениям  полей  сообщения;  –  значения  consti  ограничивают  допустимые  значения  полей;  –  выполним,  если  заданный  канал  не  пуст  и  первое  сообщение  в  канале  соответствует  всем  константным  значениям  в  операторе  приёма  сообщения.  Отправка  и  приём  сообщений  •  пример:  #define ack 5chan ch = [N] of {int, bit};bit seqno;другой вариант:ch!ack,0;ch!ack(0);ch?ack,seqnoch?ack(seqno)  Асинхронная  передача  сообщений  •  асинхронные  сообщения  буферизуются  для  последующего  приёма,  пока  канал  не  полон,  •  отправитель  блокируется,  когда  канал  полон,  •  получатель  блокируется,  когда  канал  пуст.  q!m1  q!m2  q!m3  m3  m2  q?m1  m1  q?m2  q?m3  Синхронная  передача  сообщений  •  ёмкость  канала  равна  0:  chan ch = [0] of {mtype};  •  передача  сообщений  методом  «рандеву»;  •  не  хранит  сообщения;  •  отправитель  блокируется  в  ожидании  получателя,  и  наоборот;  •  отправка  и  приём  выполняются  атомарно.  q!m1  q?m1  q!m2  q?m2  q!m3  q?m3  Пример:  моделируем  семафор  mtype = { P, V };chan sema = [0] of { mtype };active proctype semaphore(){L:sema!P -> sema?V; goto L}active [5] proctype user(){L:/*non-critical*/sema?P ->/*critical*/sema!V;goto L;}?V  !P  Другие  операции  с  каналами  •  len(q) –  возвращает  число  сообщений  в  канале,  •  empty(q) –  возвращает  true,  если  q  пуст,  •  full(q) –  возвращает  true,  если  q  полон,  •  nempty(q) –  вместо  !empty(q) (в  целях  оптимизации),  •  nfull(q) –  вместо  !full(q) (в  целях  оптимизации).

 Операции  со  скобками  •  q?[n,m,p]есть  ли  в  канале  подходящее  сообщение?  –  булево  выражение  без  побочных  эффектов,  –  равно  true,  только  когда  q?m,n,p  выполнимо,  однако  не  влияет  на  значения  n,m,p  и  не  меняет  содержимое  канала  q;    •  q?<n,m,p>широковещательный  канал  –  выполнимо  тогда  же,  когда  и  q?n,m,p;  влияет  на  значения  n,m,p  так  же,  как  и  q?n,m,p,  однако  не  меняет  содержимое  q;    •  q?n(m,p)отделяем  тип  сообщения  от  параметров  –  вариант  записи  оператора  приёма  сообщения  (т.е.  q?n,m,p),  –  может  использоваться  для  отделения  переменной  от  констант.

 Область  видимости  объявления  канала  •  имя  канала  может  быть  локальным  или  глобальным,  но  канал  сам  по  себе  –  всегда  глобальный  объект.  chan x = [3] of { chan };active proctype A(){ chan a;x?a;a!x}active proctype B(){ chan b = [2] of { chan };x!b;b?x;0}глобальная  переменная,  видна  A  и  B  неинициализированный  локальный  канал  получаем  идентификатор  канала  от  процесса  B  используем  его  инициализированный  локальный  канал  отправляем  процессу  А  идентификатор  канала  значение  x  не  изменилось  если  B  умрёт,  канал  b  исчезнет!  Особые  случаи:  упорядоченная  отправка,  случайный  приём  •  q!!n,m,p–  аналогично  q!n,m,p,  но  сообщение  n,m,p  помещается  в  канал  сразу  за  первым  сообщением,  меньшим  n,m,p;  •  q??n,m,p–  аналогично  q?n,m,p,  но  из  канала  может  быть  выбрано  любое  сообщение  (не  обязательно  первое).  init{chan q = [3] of {int};int x;q!!5;q!!2;q?x->printf(“%d\n”,x);q?x->printf(“%d\n”,x)}> ./spin sorted.pml251 process created>Основные  типы  данных  Promela  Тип  bit  bool  byte    chan  mtype  pid  short  int  unsigned  0..2n-­‐1  Диапазон  0..1    false..true  0..255    1..255    1..255    1..255    -­‐215..215-­‐1    -­‐231..231-­‐1        Пример  объявления    bit turn = 1;  bool flag = true;  byte cnt;  chan q;  mtype msg;  pid p;  short s = 100;  int x = 1;  unsigned u : 3;3  бита,  0..7  •  по  умолчанию  все  объекты  (и  локальные,  и  глобальные)  инициализируются  нулём;  •  все  переменные  должны  быть  объявлены  до  первого  использования;  •  переменная  может  быть  объявлена  где  угодно.

 Основные  типы  данных  Promela  В  Promela  нет  действительных  чисел,  чисел  с  плавающей  точкой  и  указателей.  Этот  язык  предназначен  для  описания  взаимодействия  объектов,  а  не  для  описания  вычислений.  Массивы  и  пользовательские  типы  данных  Одномерные  массивы:  byte a[27];bit flags[4] = 1;•  все  элементы  массива  инициализируются  одним  значением,  •  индексы  нумеруются  с  0.

 Пользовательские  типы  данных:typedef record {short f1;byte f2 = 4;}record rr;ff.f1 = 5;ключевое  слово  имя  пользовательского  типа  по  умолчанию  0  объявление  переменной  нового  типа  ссылка  на  элемент  структуры  Ещё  один  способ  объявления  массивов  typedef array {byte b[4];}array a[4];a[3].b[2] = 1;или  #define ab(x,y) a[x].b[y]ab(x,y) = ab(2,3) + ab(3,2);Перед  разбором  все  модели  прогоняются  через  препроцессор  С  (поддерживаются  #define,  #if,  #ifdef,  #ifndef,  #include)  Вычисление  выражений  •  Значение  всех  выражений  вычисляется  в  наиболее  широком  диапазоне  (int);  •  В  присваиваниях  и  передаче  сообщений  значения  приводятся  к  целевому  типу  после  вычисления.

 mtype = {foo, bar};active proctype tryme(){ byte x;short y = 1024;chan a,b;mtype p;}axxp====a + b;257;y;y/8Ошибка  Предупреждение  –  потеря  данных  Предупреждение  –  потеря  данных  Сообщения  об  ошибке  не  будет  Область  видимости  объектов  данных  •  Только  два  уровня  видимости:  –  глобальный  (данные  видны  всем  активным  пользователям),  –  локальный  (данные  видны  только  одному  процессу)  •  подобластей  (напр.

 для  блоков)  нет,  •  локальная  переменная  видна  везде  в  теле  процесса.  active proctype main(){ int x, y;{int y, z;x++; y++; z++};Ошибка,  повторное  объявление  y  printf(“y=%d, z=%d\n”, y, z);}Переменная  z  всё  ещё  видна!  Поток  управления  процесса  •  5  способов  задать  поток  управления:  –  последовательная  композиция  (“;”),  метки,  goto,  –  структуризация  (макросы  и  inline),  –  атомарные  последовательности  (atomic,  d_step),  –  недетерминированный  выбор  и  итерации  (if..fi,  do..od),  –  escape-­‐последовательности  ({...}unless{...}).

 Макросы  –  препроцессор  cpp  •  Используется  для  включения  файлов  и  разворачивания  макросов,  •  Варианты  использования:  –  константы  #define MAXQ 2chan q=[MAXQ] of {mtype,chan};      (альтернатива:  spin  –DMAXQ=2  …)  #define RESET(a)\–  макросы  atomic {a[0] = 0; a[1] = 0}–  условный  код  #define LOSSY 1...#ifdef LOSSYactive proctype D()#endif#if 0COMMENTS#endifМакросы  –  препроцессор  cpp  •  Минусы:    –  имена  макросов  не  видны  в  парсере,  –  имена  макросов  не  видны  при  моделировании,  •  Варианты:  –  использовать  mtype  для  определения  констант,  –  использовать  другой  препроцессор  (ключ  -­‐P),  •  inline-­‐определения.  inline-­‐определения  •  среднее  между  макросом  и  процедурой,  •  именованный  фрагмент  кода  с  параметрами,  •  не  функция  –  не  возвращает  значения.

 #define swap(a,b) tmp = a;\a = b;\b = tmp#endifinline swap(a,b){tmp = a;a = b;b = tmp}Недетерминированный  выбор  if::guard1 -> stmnt1.1;stmnt1.2;stmnt1.3;::guard2 -> stmnt2.1;stmnt2.2;stmnt2.3;::::guardn -> stmntn.1;stmntn.2;stmntn.3;fi•  оператор  if  выполним,  если  выполним  хотя  бы  один  из  стражей,  •  если  выполнимо  более  одного  стража,  то  для  выполнения  выбирается  один  из  них  недетерминированным  образом,  •  если  ни  один  из  стражей  не  выполним,  выполнение  оператора  if  блокируется,  •  в  качестве  стража  может  быть  использован  любой  оператор.

 Ещё  по  if/*ищем максимум среди x и y*/if:: x >= y -> m = x:: x <= y -> m = yfi/*случайный выбор числа 0..3*/if:: n = 0:: n = 1:: n = 2:: n = 3fiif::::::::fi(n%2 != 0)(n >= 0)(n%3 == 0)else /* ->-> n-> n-> nskip= 0= n-2= 3*/выполняется,  только  если  не  выполняется  ни  один  из  стражей  LTS  Выражение  elseC  if(x <= y)x = y – x;y++;Promela  if::(x <= y) -> x = y – x:: elsefi;y++•  в  отличие  от  С,  если  else  отсутствует,  то  выполнение  блокируется,  •  т.е.

 все  варианты  выполнения  оператора  if  должны  быть  явно  выписаны.  Специальные  выражения  и  переменные  •  else  –  true,  если  ни  один  оператор  процесса  не  выполним,  •  timeout  –  true,  если  ни  один  оператор  модели  не  выполним,  •  _    –  переменная,  доступная  только  по  записи,  значение  не  сохраняет,  •  _pid –  номер  текущего  процесса,  •  _nr_pr –  число  активных  процессов.  Оператор  dodo::guard1 -> stmnt1.1;stmnt1.2;stmnt1.3;::guard2 -> stmnt2.1;stmnt2.2;stmnt2.3;::::guardn -> stmntn.1;stmntn.2;stmntn.3;do•  в  качестве  стража  может  быть  использован  любой  оператор,  •  фактически,  это  оператор  if,  выполняемый  в  цикле  •  из  цикла  можно  выйти  только  при  помощи  break  и  goto.

 Оператор  do•  Ждём,  пока  не  наступит  момент  (a==b)  do::(a == b) -> break;::else -> skipodL:if::( a== b) -> skipelse goto Lfi(a == b)•  все  три  фрагмента  эквивалентны  Alterna“ng  Bit  Protocol    (Bartle]  и  др.,  1969)  •  Два  процесса,  отправитель  и  получатель;  •  К  каждому  сообщению  добавляется  один  бит;  •  Получатель  сообщает  о  доставке  сообщения,  возвращая  бит  отправителю;  •  Если  отправитель  убедился  в  доставке  сообщения,  он  отправляет  новое,  изменяя  значение  бита;  •  Если  значение  бита  не  изменилось,  получатель  считает,  что  идёт  повтор  сообщения.

 Функция  eval()  Отображает  текущее  значение  x  на  константу,  которая  служит  ограничением  для  принимаемых  сообщений  ch!msg(12)ch?msg(eval(x))Сообщение  будет  принято,  если  значение  переменной  x  равно  12  Модель  на  Promela  mtype = {msg, ack};chan s_r = [2] of {mtype, bit};chan r_s = [2] of {mtype, bit};active proctype sender(){ bit seqno;do:: s_r!msg,seqno ->if:: r_s?ack,eval(seqno) ->seqno = 1 - seqno;:: r_s?ack,eval(1-seqno)fiod}active proctype receiver(){ bit expect, seqno;do:: s_r?msg,seqno ->r_s!ack,seqno;if:: seqno == expect;expect = 1 - expect::elsefiodmsg(0)msg(1)ack(0)ack(1)Считываем  новое  сообщение  Сохраняем  сообщение  Игнорируем  сообщение  Запускаем  моделирование  >./spin -u20 -c abp.pmlproc 0 = senderproc 1 = receiverq\p011s_r!msg,01.s_r?msg,02.r_s!ack,02r_s?ack,01s_r!msg,11.s_r?msg,12.r_s!ack,12r_s?ack,1------------depth-limit (-u20 steps) reached------------final state:------------#processes: 2queue 1 (s_r):queue 2 (r_s):20:proc 1 (receiver) line 19"abp.pml" (state 7)20:proc 0 (sender) line7"abp.pml" (state 7)2 processes created>Моделируем  первые  20  шагов  Верификация  по  умолчанию  >./spin -a abp.pml> gcc -o pan pan.c>./pan(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claimassertion violationsacceptancecyclesinvalid end states- (none specified)+- (not selected)+State-vector 44 byte, depth reached 13, errors: 014 states, stored1 states, matched15 transitions (= stored+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)unreached in proctype senderline 15, state 10, "-end-"(1 of 10 states)unreached in proctype receiverline 27, state 10, "-end-"(1 of 10 states)Чем  и  как  проверяем?  Какие  свойства?  Проделанная  работа  Используемая  память  Обнаружен  недостижимый  код  (процессы  не  завершаются)  Графический  интерфейс  xspin  Пространства  состояний  в  SPIN  («отладка»  процесса  верификации)  Полезные  инструменты  •  Просмотр  пространства  состояний:  –  параметры  компиляции  pan.c:  •  -­‐DCHECK  –  выводить  порядок  обхода  пространства  состояний  •  -­‐DVERBOSE  -­‐DSDUMP  –  выводить  вектора  состояний  •  -­‐DBFS  –  обход  в  ширину  (удобнее  для  анализа)  –  параметры  запуска  pan:  •  -­‐d  –  вывод  графов  процессов  (state  –  номер  оператора)  •  Отключение  оптимизаций:  –  параметры  spin:  •  -­‐o1  –  отключение  оптимизации  потока  данных,  •  -­‐o2  –  отключение  удаления  мертвых  переменных,  •  -­‐o3  –  отключение  слияния  состояний  –  параметры  компиляции  pan.c:  •  -­‐DNOREDUCE  –  отключение  редукции  частичных  порядков  Обратите  внимание:  •  инициализация  переменной  (int x = 1)  не  считается  действием;  •  порождение  (run)  и  завершение  процесса  –  действия,  –  при  использовании  ac“ve  в  начальном  состоянии  процесс  уже  запущен,  –  не  только  терминальное  состояние,  но  и  терминальное  действие  -­‐end-­‐;  •  процессы  порождаются  в  случайном  порядке,  но  завершаются  в  только  порядке,  обратном  порядку  порождения  (LIFO);  •  проверка  стража  ветвления  –  действие.

 Спасибо  за  внимание!  •  Вопросы?  .