ВПнМ, примеры задач/Задача 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;
}
:: (msg == SYS_END) -> break;
:: 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 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};
<strong>bool call_irqenable;</stron>
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;
}
:: (msg == SYS_END) -> break;
:: 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;
}
Проверка свойства отсутствия тупиков
Проверка на наличие недостижимого кода
Проверка выполнения assertions
Построение контрпримера
Проверка на отсутствие циклов бездействия
Формулирование формулы LTL
Дополнительные материалы для выполнения задания
Скрипт для генерации файлов, необходимых в задании, на основании моделей
Данный скрипт генерирует файлы assert_out.txt, ver_out.txt, nonprogress_out.txt, safety_out.txt, spec.ltl на основании
