ВПнМ, примеры задач/Задача 4
Материал из eSyr's wiki.
Содержание |
[править] Задание
Для данной в третьем задании программы и её модели, построенной в ходе решения:
- Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt.
- В модели не должно быть недостижимого кода (unreachable code).
- Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt
- В модели не должно быть циклов бездействия (non-progress cycles), за исключением:
- цикла, связанного с бесконечным выполнением моделируемой функции
- циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml.
- Сформулированное в третьей задаче свойство описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. Спецификацию приложить в файле с именем spec.ltl.
a. В случае, если модель пришлось изменить:
- описать в теле письма, почему спецификация не выполняется на исходной модели;
- описать в теле письма, как изменилась модель и почему;
- описать в теле письма, почему новая модель адекватна;
- приложить контрпример, выданный pan, в файле counterexample.txt;
- приложить исходную и изменённую модели в файлах model.prm и new_model.prm;
- приложить вывод pan в файле ver_out.txt.
b. В случае, если спецификация не выполняется на модели:
- приложить контрпример, выданный pan, в файле counterexample.txt;
- построить по контрпримеру Spin контрпример на исходной программе;
- убедиться в том, что контрпример на исходной программе выполняется;
- приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных.
- приложить вывод pan в файле ver_out.txt.
c. В случае, если изменения в модели не потребовались и спецификация выполняется:
- приложить модель в файле model.prm;
- приложить вывод pan в файле ver_out.txt.
Во всех случаях письмо должно удовлетворять требованиям:
- письмо написано в формате plain/text без html;
- в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и utf8 (желательно в кодировке koi8-r).
- к письму должна прилагаться формулировка третьей задачи с файле с именем task3.txt
[править] Вариант 1
Также см. Задание 3, вариант 1.
[править] Исходный текст функции
PRIVATE int DspVersion[2];
PRIVATE int dsp_init()
{
int i, s;
if(dsp_reset () != OK) {
dprint("sb16: No SoundBlaster card detected\n");
return -1;
}
DspVersion[0] = DspVersion[1] = 0;
dsp_command(DSP_GET_VERSION); /* Get DSP version bytes */
for(i = 1000; i; i--) {
if(sb16_inb(DSP_DATA_AVL) & 0x80) {
if(DspVersion[0] == 0) {
DspVersion[0] = sb16_inb(DSP_READ);
} else {
DspVersion[1] = sb16_inb(DSP_READ);
break;
}
}
}
if(DspVersion[0] < 4) {
dprint("sb16: No SoundBlaster 16 compatible card detected\n");
return -1;
}
dprint("sb16: SoundBlaster DSP version %d.%d detected\n", DspVersion[0], DspVersion[1]);
/* set SB to use our IRQ and DMA channels */
mixer_set(MIXER_SET_IRQ, (1 << (SB_IRQ / 2 - 1)));
mixer_set(MIXER_SET_DMA, (1 << SB_DMA_8 | 1 << SB_DMA_16));
/* register interrupt vector and enable irq */
if ((s=sys_irqsetpolicy(SB_IRQ, IRQ_REENABLE, &irq_hook_id )) != OK)
panic("SB16DSP", "Couldn't set IRQ policy", s);
if ((s=sys_irqenable(&irq_hook_id)) != OK)
panic("SB16DSP", "Couldn't enable IRQ", s);
DspAvail = 1;
return OK;
}
[править] Свойства корректности
Модель должна быть адекватной для проверки спецификации: всегда при вызове sys_irqenable верно DspVersion[0] < 4
[править] Исходная модель
#define OK 0
#define NOT_OK 1
#define SYS_IRQPOLICY 1
#define SYS_IRQENABLE 2
int DspVersion[2];
chan to_kernel_channel = [0] of {byte};
chan from_kernel_channel = [0] of {byte};
active proctype kernel()
{
int msg;
do
:: to_kernel_channel?msg ->
{
if
:: (msg == SYS_IRQPOLICY) ->
{
if
:: from_kernel_channel!OK;
:: from_kernel_channel!NOT_OK;
fi;
}
:: (msg == SYS_IRQENABLE) ->
{
if
:: from_kernel_channel!OK;
:: from_kernel_channel!NOT_OK;
fi;
}
:: else -> skip;
fi;
}
od;
}
active proctype dsp_init()
{
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) */
to_kernel_channel!SYS_IRQENABLE;
from_kernel_channel?result;
if :: (result != OK) ->
{
goto return;
}
:: else -> skip;
fi;
return:
skip;
od;
}
[править] Решение
[править] Модифицированная модель
В модель внесены следующие модификации:
- Добавлен assert для проверки спецификации
- Добавлены метки progress для внешних циклов у каждого процесса, так как они должны быть бесконечными
- Добавлены глобальные переменные и их изменение для верификации модели с использованием LTL, а также define тех символов, которые использовались в формуле
#define OK 0
#define NOT_OK 1
#define SYS_IRQPOLICY 1
#define SYS_IRQENABLE 2
#define p (call_irqenable == true)
#define q (DspVersion[0] < 4)
int DspVersion[2];
chan to_kernel_channel = [0] of {byte};
chan from_kernel_channel = [0] of {byte};
bool call_irqenable;
active proctype kernel()
{
int msg;
progress:
do
:: to_kernel_channel?msg ->
{
if
:: (msg == SYS_IRQPOLICY) ->
{
if
:: from_kernel_channel!OK;
:: from_kernel_channel!NOT_OK;
fi;
}
:: (msg == SYS_IRQENABLE) ->
{
assert(DspVersion[0] < 4);
if
:: from_kernel_channel!OK;
:: from_kernel_channel!NOT_OK;
fi;
}
:: else -> skip;
fi;
}
od;
}
active proctype dsp_init()
{
progress:
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) */
call_irqenable = true;
to_kernel_channel!SYS_IRQENABLE;
from_kernel_channel?result;
call_irqenable = false;
if :: (result != OK) ->
{
goto return;
}
:: else -> skip;
fi;
return:
skip;
od;
}
[править] Проверка свойства отсутствия тупиков
- Для проверки этого свойства достаточно включить во время верификации проверку на invalid end-states, точнее, не выключать её. То есть, достаточно не трогать флаг -Eю Так же, если в модели уже присутствуют ассерты, стоит добавить флаг -A, чтобы их игнорировать.
Пример проверки:
% spin -a new_model.prm
% gcc -DSAFETY pan.c -o pan
% ./pan -A
(Spin Version 5.1.4 -- 27 January 2008)
+ Partial Order Reduction
Full statespace search for:
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
66 states, stored
11 states, matched
77 transitions (= stored+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
[править] Проверка на наличие недостижимого кода
Эта проверка выполняется одновременно с предыдущей. В выводе pan не должно быть сообщений о недостижимом коде (unreached code), кроме завершительных состояний каждого из процессов, крутящихся в бесконечном цикле.
[править] Проверка выполнения assertions
Достаточно собрать pan и выполнить без флага -A. При этом, в зависимости от программы и спецификации, assert может как произойти, так и не произойти:
% spin -a model_assert.prm
% gcc -DSAFETY pan.c -o pan
% ./pan -E
pan: assertion violated (DspVersion[0]<4) (at depth 17)
pan: wrote model_assert.prm.trail
(Spin Version 5.1.4 -- 27 January 2008)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by -E flag)
State-vector 36 byte, depth reached 17, errors: 1
33 states, stored
5 states, matched
38 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
2.501 memory usage (Mbyte)
pan: elapsed time 0 seconds
[править] Построение контрпримера
Если assertion произошёл, то необходимо исследовать контрпример и показать, что он является контрпримером для исходной программы (а не является следствием ошибки моделирования). Сам контрпример сохранился в файле model_assert.prm, как указано в выводе pan выше. Для наглядного рассмотрения контрпримера можно сделать следующее:
% spin -p -tmodel_assert.prm.trail model_assert.prm
Starting kernel with pid 0
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
Далее, надо построить контрпример для программы, основываясь на полученной трассе. Методом пристального вглядывания можно узнать, что случилось следующее: в процессе инициализации значения DspCersion[0] оно получило значение 5, и при вызове системного вызова спецификация нарушилась. Это и надо отразить в контрпримере, например, так (пример файла prog_counterexample.txt):
Номера строк даны в соответствии с prog.c Строка DspVersion[0] 7 --- 12 0 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(), и, как следствие, спецификация нарушается, что и было выявлено в процессе верификации модели.
[править] Проверка на отсутствие циклов бездействия
Проверка на отсутствие циклов бездействия осуществляется после помечания всех циклов, которые должны быть бесконечными, меткой progress, для поиска других бесконечных циклов, которых быть не болжно. Пример вывода, когда таких циклов больше нет:
% 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
При этом надо учитывать, что для проверки существования таких циклов необходимо изменить параметры верификации (в частности, отключить справедливость диспечеризации). Поэтому параметры компиляции pan и его запуска должны быть соответствующими (проверка на циклы бездействия осуществляется ключом -l). Также стоит отключить проверку assertions (-A).
[править] Формулирование формулы LTL
Сначала, необходимо выразить спецификацию на языке LTL (это относительно творческая часть). В процессе окажется, что для проверки с использованием LTL необходимо задействовать ряд глобальных флагов, их стоит добавить. Каждую булеву формулу стоит описать отдельно в виде define. В заключение, можно сказать следующее:
% spin -f '<> (p && !q)'
never { /* <> (p && !q) */
T0_init:
if
:: (! ((q)) && (p)) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all:
skip
}
Важно помнить, что формулируется отрицание спецификации, то есть то, как модель себя вести не должна. Простой путь --- сформулировать специйикацию, взять в скобки и поставить в переди знак отрицания. Преобразовать полученую LTL-формулу можно по вкусу.
Полученную конструкцию never стоит проверить на модели. Результат верификации должен быть такой же, как при использовании assertions (если модель выполняется, то он должна выполняться, если нет --- то нет):
% 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)
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)
pan: elapsed time 0 seconds
[править] Дополнительные материалы для выполнения задания
[править] Скрипт для генерации файлов, необходимых в задании, на основании моделей
Данный скрипт генерирует файлы assert_out.txt, ver_out.txt, nonprogress_out.txt, safety_out.txt, spec.ltl на основании моделей (model.prm, new_model.prm, model_assert.prm) и формулы (формула должна находиться в formulae.ltl или передаваться в качестве параметра).
#! /bin/sh
spin -a model.prm
gcc -DSAFETY pan.c -o pan
./pan > ver_out.txt
spin -a new_model.prm
gcc -DSAFETY pan.c -o pan
./pan -A > safety_out.txt
spin -a model_assert.prm
gcc -DSAFETY pan.c -o pan
./pan -E > assert_out.txt
gcc -DNP pan.c -o pan
./pan -l -A > nonprogress_out.txt
spin -f "${1:-`cat formulae.ltl`}" > spec.ltl
spin -a -N spec.ltl model_assert.prm
gcc pan.c -o pan
./pan -a -A > ltl_check.txt
[править] Скрипт для генерации дистрибутива
Данный скрипт помещает файлы, необходимые для отправки, в поддиректорию distr/. Если раскомментировать последнюю строку, то дополнительно будет создан архив, содержащий все эти файлы.
#! /bin/sh
mkdir distr
cp spec.ltl task3.txt model.prm new_model.prm model_assert.prm assert_out.txt nonprogress_out.txt safety_out.txt ver_out.txt counterexample.txt prog_counterexample.txt distr/
#tar -jcf ${1:-distr}.tar.bz2 distr/
