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

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

(Различия между версиями)

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

Версия 22:17, 25 апреля 2008

Содержание

1 Задание
2 Вариант 1

Задание

Для данной в третьем задании программы и её модели, построенной в ходе решения:

Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt.
В модели не должно быть недостижимого кода (unreachable code).
Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt
В модели не должно быть циклов бездействия (non-progress cycles), за исключением:
1. цикла, связанного с бесконечным выполнением моделируемой функции
2. циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем 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/

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

01 02 03 04 05 06 07 08 09 10

Календарь