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

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

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

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

Версия 20:25, 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;
        }
        :: (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 на основании моделей (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

Календарь