Редактирование: ВПнМ, примеры задач/Задача 4

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

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 125: Строка 125:
fi;
fi;
}
}
 +
:: (msg == SYS_END) -> break;
:: else -> skip;
:: else -> skip;
fi;
fi;
Строка 192: Строка 193:
* Добавлен assert для проверки спецификации
* Добавлен assert для проверки спецификации
* Добавлены метки progress для внешних циклов у каждого процесса, так как они должны быть бесконечными
* Добавлены метки progress для внешних циклов у каждого процесса, так как они должны быть бесконечными
-
* Добавлены глобальные переменные и их изменение для верификации модели с использованием LTL, а также define тех символов, которые использовались в формуле
+
* Добавлены глобальные переменные и их изменение для верификации модели с использованием LTL
-
#define OK 0
+
<pre>#define OK 0
-
#define NOT_OK 1
+
#define NOT_OK 1
-
+
-
#define SYS_IRQPOLICY 1
+
-
#define SYS_IRQENABLE 2
+
-
+
-
<strong>#define p (call_irqenable == true)
+
-
#define q (DspVersion[0] < 4)</strong>
+
-
+
-
int DspVersion[2];
+
-
+
-
chan to_kernel_channel = [0] of {byte};
+
-
chan from_kernel_channel = [0] of {byte};
+
-
+
-
<strong>bool call_irqenable;</strong>
+
-
+
-
active proctype kernel()
+
-
{
+
-
int msg;
+
-
+
-
<strong>progress:</strong>
+
-
do
+
-
:: to_kernel_channel?msg ->
+
-
{
+
-
if
+
-
:: (msg == SYS_IRQPOLICY) ->
+
-
{
+
-
if
+
-
:: from_kernel_channel!OK;
+
-
:: from_kernel_channel!NOT_OK;
+
-
fi;
+
-
}
+
-
:: (msg == SYS_IRQENABLE) ->
+
-
{
+
-
<strong>assert(DspVersion[0] < 4);</strong>
+
-
if
+
-
:: from_kernel_channel!OK;
+
-
:: from_kernel_channel!NOT_OK;
+
-
fi;
+
-
}
+
-
:: else -> skip;
+
-
fi;
+
-
}
+
-
od;
+
-
}
+
-
+
-
active proctype dsp_init()
+
-
{
+
-
<strong>progress:</strong>
+
-
do
+
-
::
+
-
byte result;
+
-
+
-
DspVersion[0] = 0;
+
-
DspVersion[1] = 0;
+
-
+
-
if
+
-
:: DspVersion[0] = 0;
+
-
:: DspVersion[0] = 1;
+
-
:: DspVersion[0] = 5;
+
-
fi;
+
-
+
-
if
+
-
:: DspVersion[1] = 0;
+
-
:: DspVersion[1] = 1;
+
-
fi;
+
-
+
-
if :: (DspVersion[0] < 4) ->
+
-
{
+
-
goto return;
+
-
}
+
-
:: else -> skip;
+
-
fi;
+
-
+
-
/* sys_irqsetpolicy(SB_IRQ, IRQ_REENABLE, &irq_hook_id); */
+
-
to_kernel_channel!SYS_IRQPOLICY;
+
-
from_kernel_channel?result;
+
-
+
-
if
+
-
:: (result != OK) ->
+
-
{
+
-
goto return;
+
-
}
+
-
:: else -> skip;
+
-
fi;
+
-
+
-
/* sys_irqenable(&irq_hook_id) */
+
-
<strong>call_irqenable = true;</strong>
+
-
to_kernel_channel!SYS_IRQENABLE;
+
-
from_kernel_channel?result;
+
-
<strong>call_irqenable = false;</strong>
+
-
+
-
if :: (result != OK) ->
+
-
{
+
-
goto return;
+
-
}
+
-
:: else -> skip;
+
-
fi;
+
-
+
-
return:
+
-
skip;
+
-
od;
+
-
}
+
-
+
-
==== Проверка свойства отсутствия тупиков ====
+
-
* Для проверки этого свойства достаточно включить во время верификации проверку на invalid end-states, точнее, не выключать её. То есть, достаточно не трогать флаг -Eю Так же, если в модели уже присутствуют ассерты, стоит добавить флаг -A, чтобы их игнорировать.
+
-
Пример проверки:
+
#define SYS_IRQPOLICY 1
-
<pre>% spin -a new_model.prm
+
#define SYS_IRQENABLE 2
-
% gcc -DSAFETY pan.c -o pan
+
-
% ./pan -A
+
-
(Spin Version 5.1.4 -- 27 January 2008)
+
-
+ Partial Order Reduction
+
-
Full statespace search for:
+
int DspVersion[2];
-
never claim - (none specified)
+
-
assertion violations - (disabled by -A flag)
+
-
cycle checks - (disabled by -DSAFETY)
+
-
invalid end states +
+
-
State-vector 36 byte, depth reached 24, errors: 0
+
chan to_kernel_channel = [0] of {byte};
-
66 states, stored
+
chan from_kernel_channel = [0] of {byte};
-
11 states, matched
+
-
77 transitions (= stored+matched)
+
-
0 atomic steps
+
-
hash conflicts: 0 (resolved)
+
-
2.501 memory usage (Mbyte)
+
<strong>bool call_irqenable;</stron>
-
unreached in proctype kernel
+
active proctype kernel()
-
line 45, state 23, "-end-"
+
{
-
(1 of 23 states)
+
int msg;
-
unreached in proctype dsp_init
+
-
line 103, state 43, "-end-"
+
-
(1 of 43 states)
+
-
pan: elapsed time 0 seconds
+
<strong>progress:</strong>
-
</pre>
+
do
 +
:: to_kernel_channel?msg ->
 +
{
 +
if
 +
:: (msg == SYS_IRQPOLICY) ->
 +
{
 +
if
 +
:: from_kernel_channel!OK;
 +
:: from_kernel_channel!NOT_OK;
 +
fi;
 +
}
 +
:: (msg == SYS_IRQENABLE) ->
 +
{
 +
<strong>assert(DspVersion[0] < 4);</strong>
 +
if
 +
:: from_kernel_channel!OK;
 +
:: from_kernel_channel!NOT_OK;
 +
fi;
 +
}
 +
:: (msg == SYS_END) -> break;
 +
:: else -> skip;
 +
fi;
 +
}
 +
od;
 +
}
-
==== Проверка на наличие недостижимого кода ====
+
active proctype dsp_init()
-
Эта проверка выполняется одновременно с предыдущей. В выводе pan не должно быть сообщений о недостижимом коде (unreached code), кроме завершительных состояний каждого из процессов, крутящихся в бесконечном цикле.
+
{
 +
<strong>progress:</strong>
 +
do
 +
::
 +
byte result;
-
==== Проверка выполнения assertions ====
+
DspVersion[0] = 0;
-
Достаточно собрать pan и выполнить без флага -A. При этом, в зависимости от программы и спецификации, assert может как произойти, так и не произойти:
+
DspVersion[1] = 0;
-
<pre>% spin -a model_assert.prm
+
-
% gcc -DSAFETY pan.c -o pan
+
-
% ./pan -E
+
-
pan: assertion violated (DspVersion[0]<4) (at depth 17)
+
if
-
pan: wrote model_assert.prm.trail
+
:: DspVersion[0] = 0;
 +
:: DspVersion[0] = 1;
 +
:: DspVersion[0] = 5;
 +
fi;
-
(Spin Version 5.1.4 -- 27 January 2008)
+
if
-
Warning: Search not completed
+
:: DspVersion[1] = 0;
-
+ Partial Order Reduction
+
:: DspVersion[1] = 1;
 +
fi;
-
Full statespace search for:
+
if :: (DspVersion[0] < 4) ->
-
never claim - (none specified)
+
{
-
assertion violations +
+
goto return;
-
cycle checks - (disabled by -DSAFETY)
+
}
-
invalid end states - (disabled by -E flag)
+
:: else -> skip;
 +
fi;
-
State-vector 36 byte, depth reached 17, errors: 1
+
/* sys_irqsetpolicy(SB_IRQ, IRQ_REENABLE, &irq_hook_id); */
-
33 states, stored
+
to_kernel_channel!SYS_IRQPOLICY;
-
5 states, matched
+
from_kernel_channel?result;
-
38 transitions (= stored+matched)
+
-
0 atomic steps
+
-
hash conflicts: 0 (resolved)
+
-
2.501 memory usage (Mbyte)
+
if
 +
:: (result != OK) ->
 +
{
 +
goto return;
 +
}
 +
:: else -> skip;
 +
fi;
 +
/* sys_irqenable(&irq_hook_id) */
 +
<strong>call_irqenable = true;</strong>
 +
to_kernel_channel!SYS_IRQENABLE;
 +
from_kernel_channel?result;
 +
<strong>call_irqenable = false;</strong>
-
pan: elapsed time 0 seconds</pre>
+
if :: (result != OK) ->
-
 
+
{
-
===== Построение контрпримера =====
+
goto return;
-
Если assertion произошёл, то необходимо исследовать контрпример и показать, что он является контрпримером для исходной программы (а не является следствием ошибки моделирования). Сам контрпример сохранился в файле model_assert.prm, как указано в выводе pan выше. Для наглядного рассмотрения контрпримера можно сделать следующее:
+
}
-
<pre>% spin -p -tmodel_assert.prm.trail model_assert.prm
+
:: else -> skip;
-
Starting kernel with pid 0
+
fi;
-
Starting dsp_init with pid 1
+
-
spin: couldn't find claim (ignored)
+
-
2: proc 1 (dsp_init) line 54 "model_assert.prm" (state 1) [DspVersion[0] = 0]
+
-
4: proc 1 (dsp_init) line 55 "model_assert.prm" (state 2) [DspVersion[1] = 0]
+
-
6: proc 1 (dsp_init) line 60 "model_assert.prm" (state 5) [DspVersion[0] = 5]
+
-
8: proc 1 (dsp_init) line 64 "model_assert.prm" (state 8) [DspVersion[1] = 0]
+
-
10: proc 1 (dsp_init) line 72 "model_assert.prm" (state 15) [else]
+
-
12: proc 1 (dsp_init) line 72 "model_assert.prm" (state 16) [(1)]
+
-
14: proc 1 (dsp_init) line 76 "model_assert.prm" (state 19) [to_kernel_channel!1]
+
-
15: proc 0 (kernel) line 23 "model_assert.prm" (state 1) [to_kernel_channel?msg]
+
-
17: proc 0 (kernel) line 26 "model_assert.prm" (state 2) [((msg==1))]
+
-
19: proc 0 (kernel) line 29 "model_assert.prm" (state 3) [from_kernel_channel!0]
+
-
20: proc 1 (dsp_init) line 77 "model_assert.prm" (state 20) [from_kernel_channel?result]
+
-
22: proc 1 (dsp_init) line 84 "model_assert.prm" (state 24) [else]
+
-
24: proc 1 (dsp_init) line 84 "model_assert.prm" (state 25) [(1)]
+
-
26: proc 1 (dsp_init) line 88 "model_assert.prm" (state 28) [call_irqenable = 1]
+
-
28: proc 1 (dsp_init) line 89 "model_assert.prm" (state 29) [to_kernel_channel!2]
+
-
29: proc 0 (kernel) line 23 "model_assert.prm" (state 1) [to_kernel_channel?msg]
+
-
spin: trail ends after 30 steps
+
-
#processes: 2
+
-
DspVersion[0] = 5
+
-
DspVersion[1] = 0
+
-
call_irqenable = 1
+
-
30: proc 1 (dsp_init) line 90 "model_assert.prm" (state 30)
+
-
30: proc 0 (kernel) line 43 "model_assert.prm" (state 19)
+
-
2 processes created</pre>
+
-
 
+
-
Далее, надо построить контрпример для программы, основываясь на полученной трассе. Методом пристального вглядывания можно узнать, что случилось следующее: в процессе инициализации значения DspCersion[0] оно получило значение 5, и при вызове системного вызова спецификация нарушилась. Это и надо отразить в контрпримере, например, так (пример файла prog_counterexample.txt):
+
-
<pre>Номера строк даны в соответствии с prog.c
+
-
Строка DspVersion[0]
+
return:
-
7 ---
+
skip;
-
12 0
+
od;
-
13 0
+
-
15 0
+
-
16 0
+
-
17 0
+
-
18 5
+
-
15 5
+
-
16 5
+
-
17 5
+
-
20 5
+
-
21 5
+
-
26 5
+
-
31 5
+
-
35 5
+
-
36 5
+
-
39 5
+
-
41 5
+
-
 
+
-
На 41 строке происходит вызов sys_irqenable(), и, как следствие, спецификация нарушается, что и было выявлено в процессе верификации модели.
+
-
</pre>
+
-
 
+
-
==== Проверка на отсутствие циклов бездействия ====
+
-
Проверка на отсутствие циклов бездействия осуществляется после помечания всех циклов, которые должны быть бесконечными, меткой progress, для поиска других бесконечных циклов, которых быть не болжно. Пример вывода, когда таких циклов больше нет:
+
-
<pre>% spin -a model_assert.prm
+
-
% gcc -DNP pan.c -o pan
+
-
% ./pan -l -A
+
-
(Spin Version 5.1.4 -- 27 January 2008)
+
-
+ Partial Order Reduction
+
-
 
+
-
Full statespace search for:
+
-
never claim +
+
-
assertion violations - (disabled by -A flag)
+
-
non-progress cycles + (fairness disabled)
+
-
invalid end states - (disabled by never claim)
+
-
 
+
-
State-vector 44 byte, depth reached 45, errors: 0
+
-
80 states, stored (94 visited)
+
-
22 states, matched
+
-
116 transitions (= visited+matched)
+
-
0 atomic steps
+
-
hash conflicts: 0 (resolved)
+
-
 
+
-
2.501 memory usage (Mbyte)
+
-
 
+
-
unreached in proctype kernel
+
-
line 45, state 23, "-end-"
+
-
(1 of 23 states)
+
-
unreached in proctype dsp_init
+
-
line 103, state 43, "-end-"
+
-
(1 of 43 states)
+
-
 
+
-
pan: elapsed time 0 seconds
+
-
</pre>
+
-
 
+
-
При этом надо учитывать, что для проверки существования таких циклов необходимо изменить параметры верификации (в частности, отключить справедливость диспечеризации). Поэтому параметры компиляции pan и его запуска должны быть соответствующими (проверка на циклы бездействия осуществляется ключом -l). Также стоит отключить проверку assertions (-A).
+
-
 
+
-
==== Формулирование формулы LTL ====
+
-
Сначала, необходимо выразить спецификацию на языке LTL (это относительно творческая часть). В процессе окажется, что для проверки с использованием LTL необходимо задействовать ряд глобальных флагов, их стоит добавить. Каждую булеву формулу стоит описать отдельно в виде define. В заключение, можно сказать следующее:
+
-
<pre>% spin -f '<> (p && !q)'
+
-
never { /* <> (p && !q) */
+
-
T0_init:
+
-
if
+
-
:: (! ((q)) && (p)) -> goto accept_all
+
-
:: (1) -> goto T0_init
+
-
fi;
+
-
accept_all:
+
-
skip
+
}</pre>
}</pre>
-
Важно помнить, что формулируется отрицание спецификации, то есть то, как модель себя вести не должна. Простой путь --- сформулировать специйикацию, взять в скобки и поставить в переди знак отрицания. Преобразовать полученую LTL-формулу можно по вкусу.
+
==== Проверка свойства отсутствия тупиков ====
-
Полученную конструкцию never стоит проверить на модели. Результат верификации должен быть такой же, как при использовании assertions (если модель выполняется, то он должна выполняться, если нет --- то нет):
+
==== Проверка на наличие недостижимого кода ====
-
<pre>% spin -f '<> (p && !q)' > spec.ltl
+
-
% spin -a -N spec.ltl model_assert.prm
+
-
% gcc pan.c -o pan
+
-
% ./pan -a -A
+
-
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+
-
(never claims generated from LTL formulae are stutter-invariant)
+
-
pan: claim violated! (at depth 30)
+
-
pan: wrote model_assert.prm.trail
+
-
(Spin Version 5.1.4 -- 27 January 2008)
+
==== Проверка выполнения assertions ====
-
Warning: Search not completed
+
-
+ Partial Order Reduction
+
-
Full statespace search for:
+
===== Построение контрпримера =====
-
never claim +
+
-
assertion violations - (disabled by -A flag)
+
-
acceptance cycles + (fairness disabled)
+
-
invalid end states - (disabled by never claim)
+
-
State-vector 44 byte, depth reached 30, errors: 1
+
==== Проверка на отсутствие циклов бездействия ====
-
32 states, stored
+
-
5 states, matched
+
-
37 transitions (= stored+matched)
+
-
0 atomic steps
+
-
hash conflicts: 0 (resolved)
+
-
2.501 memory usage (Mbyte)
+
==== Формулирование формулы LTL ====
-
 
+
-
 
+
-
pan: elapsed time 0 seconds
+
-
</pre>
+
== Дополнительные материалы для выполнения задания ==
== Дополнительные материалы для выполнения задания ==

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!


Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_%D0%BF%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_4
Личные инструменты
Разделы