ВПнМ, примеры задач/Задача 2

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: == Задание == Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель ...)
м (Вывод spin)
 
(1 промежуточная версия не показана)
Строка 5: Строка 5:
Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором.
Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором.
-
== Варианты ==
+
== Вариант 1 ==
void
void
f (int a, int b, int c)
f (int a, int b, int c)
Строка 81: Строка 81:
==== Вывод spin ====
==== Вывод spin ====
-
spin -a task2.pml
+
% spin -a task2.pml
-
gcc -DSAFETY pan.c -o pan
+
% gcc -DSAFETY pan.c -o pan
-
./pan > log
+
% ./pan > log
(Spin Version 5.1.4 -- 27 January 2008)
(Spin Version 5.1.4 -- 27 January 2008)
+ Partial Order Reduction
+ Partial Order Reduction

Текущая версия

Содержание

[править] Задание

Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа состояний этой модели.

Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором.

[править] Вариант 1

void
f (int a, int b, int c)
{
 int x = 0, y = 0, z = 0;
 x = 4;
 y = 1;
 z = a;
 if (y > 6)
   {
    x = 2;
     z = y + x;
     if (z > c)
       {
         x = 10;
       }
     if (y > 6)
       {
          z = b;
       }
     else
       {
         x = 5;
       }
     y = 2;
     y = 2;
   }
 y = 2;
}

[править] Решение

[править] Модель

proctype f (int a; int b; int c)
{
 int x = 0, y = 0, z = 0;
 x = 4;
 y = 1;
 z = a;
 if :: (y > 6) ->
   {
     x = 2;
     z = y + x;
     if :: (z > c) ->
       {
         x = 10;
       }
     :: else ->
       {
         skip;
       }
     fi;
     if :: (y > 6) ->
       {
         z = b;
       }
     :: else
       {
         x = 5;
       }
     fi;
     y = 2;
     y = 2;
   }
   :: else -> skip;
   fi;
 y = 2; 
}

active proctype main()
{
   run f(1,2,3);
}

[править] Вывод spin

% spin -a task2.pml
% gcc -DSAFETY pan.c -o pan
% ./pan > log
(Spin Version 5.1.4 -- 27 January 2008)
        + Partial Order Reduction  

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      +  

State-vector 40 byte, depth reached 6, errors: 0
        7 states, stored
        0 states, matched
        7 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)   

    2.501       memory usage (Mbyte)   

unreached in proctype f
        line 14, state 9, "x = 10"
        line 18, state 12, "(1)"
        line 11, state 13, "((z>c))"
        line 11, state 13, "else"
        line 20, state 21, "((y>6))"
        line 20, state 21, "else"
        line 31, state 25, "x = 2"
        (5 of 31 states)
unreached in proctype main
        (0 of 2 states)  

pan: elapsed time 0 seconds

Cогласно верификатору, у модели --- 7 достижимых состояний.

[править] Как моделировать различные конструкции

[править] if

Если if имеет одну ветку, то конструкция на С

if (condition)
{
  expression;
}

Преобразуется в слудующую конструкцию на Promela:

if :: condition ->
{
  expression;
}
:: else -> skip;
fi;

Где:

  • if ... fi --- конструкция, порождающая недетерминизм --- выполняется любая возможная ветвь
  •  :: .... --- ветвь недетерминированной конструкции
  • condition --- условие-страж --- ветвь не выполнится при ложном условии
  • else --- ветка, которая выполняется, если все стражи ложны
  • skip --- пустой оператор

Как следствие, если условие истинно, всегда выполняется первая ветвь, если нет --- вторая.

Аналогично, if с обеими ветвями моделируется следующим образом:

if :: condition ->
{
  expression;
}
:: else ->
{
  else_expression;
}
fi;

[править] Функции

  • Процессы, работающие на протяжении всей работы программы, обычно моделируют как active proctype. Подобные функции не принимают параметров
  • Если необходимо передать параметры процессу (и/или смоделировать недетерминизм в их значении), то можно использовать типы функций inline или proctype. Первый вызывается так: func(), второй --- так: run func(). При этом inline рассматривается как некий аналог макроса, а proctype --- ещё один процесс, который запускается командой run


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин

Разделы