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

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

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

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

Версия 10:01, 25 апреля 2008

Содержание

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

Задача

Дано:

исходный текст функции
свойства корректности

Требуется построить корректную модель функции, адекватную заданному свойству корректности. Требуется построить модель с двумя процессами: ядром, отвечающим на эти системные вызовы; функцией, работающей в цикле. Системные вызовы и ответ на них моделируются посылкой сообщения ядру и приёмом сообщения от ядра соответственно.

Результат:

текст модели на языке Promela
скриншот диаграммы состояний, полученной в результате моделирования (первые 40 шагов)
вывод моделирования (первые 40 шагов)

Вариант 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;
}

Вывод симулирования

Cкриншот диаграммы состояний

% spin -p -u40 model.pml  
spin: line  34 "model.pml", Error: undeclared variable: SYS_END saw '')' = '41''
Starting kernel with pid 0
  0:    proc  - (:root:) creates proc  0 (kernel)
Starting dsp_init with pid 1
  0:    proc  - (:root:) creates proc  1 (dsp_init)
  1:    proc  1 (dsp_init) line  43 "model.pml" (state 38)      [DspVersion[0] = 0]
  2:    proc  1 (dsp_init) line  48 "model.pml" (state 2)       [DspVersion[1] = 0]
  3:    proc  1 (dsp_init) line  50 "model.pml" (state 6)       [DspVersion[0] = 0]
  4:    proc  1 (dsp_init) line  56 "model.pml" (state 7)       [.(goto)]
  5:    proc  1 (dsp_init) line  56 "model.pml" (state 10)      [DspVersion[1] = 0]
  6:    proc  1 (dsp_init) line  61 "model.pml" (state 11)      [.(goto)]
  7:    proc  1 (dsp_init) line  61 "model.pml" (state 17)      [((DspVersion[0]<4))]
  8:    proc  1 (dsp_init) line  64 "model.pml" (state 14)      [goto return]
  9:    proc  1 (dsp_init) line  92 "model.pml" (state 37)      [(1)]
 10:    proc  1 (dsp_init) line  94 "model.pml" (state 39)      [.(goto)]
 11:    proc  1 (dsp_init) line  43 "model.pml" (state 38)      [DspVersion[0] = 0]
 12:    proc  1 (dsp_init) line  48 "model.pml" (state 2)       [DspVersion[1] = 0]
 13:    proc  1 (dsp_init) line  50 "model.pml" (state 6)       [DspVersion[0] = 1]
 14:    proc  1 (dsp_init) line  56 "model.pml" (state 7)       [.(goto)]
 15:    proc  1 (dsp_init) line  56 "model.pml" (state 10)      [DspVersion[1] = 0]
 16:    proc  1 (dsp_init) line  61 "model.pml" (state 11)      [.(goto)]
 17:    proc  1 (dsp_init) line  61 "model.pml" (state 17)      [((DspVersion[0]<4))]
 18:    proc  1 (dsp_init) line  64 "model.pml" (state 14)      [goto return]
 19:    proc  1 (dsp_init) line  92 "model.pml" (state 37)      [(1)]
 20:    proc  1 (dsp_init) line  94 "model.pml" (state 39)      [.(goto)]
 21:    proc  1 (dsp_init) line  43 "model.pml" (state 38)      [DspVersion[0] = 0]
 22:    proc  1 (dsp_init) line  48 "model.pml" (state 2)       [DspVersion[1] = 0]
 23:    proc  1 (dsp_init) line  50 "model.pml" (state 6)       [DspVersion[0] = 1]
 24:    proc  1 (dsp_init) line  56 "model.pml" (state 7)       [.(goto)]
 25:    proc  1 (dsp_init) line  56 "model.pml" (state 10)      [DspVersion[1] = 0]
 26:    proc  1 (dsp_init) line  61 "model.pml" (state 11)      [.(goto)]
 27:    proc  1 (dsp_init) line  61 "model.pml" (state 17)      [((DspVersion[0]<4))]
 28:    proc  1 (dsp_init) line  64 "model.pml" (state 14)      [goto return]
 29:    proc  1 (dsp_init) line  92 "model.pml" (state 37)      [(1)]
 30:    proc  1 (dsp_init) line  94 "model.pml" (state 39)      [.(goto)]
 31:    proc  1 (dsp_init) line  43 "model.pml" (state 38)      [DspVersion[0] = 0]
 32:    proc  1 (dsp_init) line  48 "model.pml" (state 2)       [DspVersion[1] = 0]
 33:    proc  1 (dsp_init) line  50 "model.pml" (state 6)       [DspVersion[0] = 5]
 34:    proc  1 (dsp_init) line  56 "model.pml" (state 7)       [.(goto)]
 35:    proc  1 (dsp_init) line  56 "model.pml" (state 10)      [DspVersion[1] = 1]
 36:    proc  1 (dsp_init) line  61 "model.pml" (state 11)      [.(goto)]
 37:    proc  1 (dsp_init) line  61 "model.pml" (state 17)      [else]
 38:    proc  1 (dsp_init) line  65 "model.pml" (state 16)      [(1)]
 39:    proc  1 (dsp_init) line  69 "model.pml" (state 18)      [.(goto)]
 40:    proc  1 (dsp_init) line  69 "model.pml" (state 19)      [to_kernel_channel!1]
 40:    proc  0 (kernel) line  17 "model.pml" (state 1) [to_kernel_channel?msg]
-------------
depth-limit (-u40 steps) reached
#processes: 2
                DspVersion[0] = 5
                DspVersion[1] = 1
 40:    proc  1 (dsp_init) line  70 "model.pml" (state 20)
 40:    proc  0 (kernel) line  19 "model.pml" (state 18)
2 processes created

Пояснения

Абстрагирование

В модели необходимо абстрагироваться ото всего, что не влияет на спецификацию. При этом надо учитывать, что, на первый взгляд посторонние переменные могут значимо влиять на поток управления и при их абстрагировании корректность и адекватность модели могут нарушаться.

Недетерминизм

Если необходимо проверить все возможные варианты, индуцированные различными значениями переменных, надо выделить различимые множества значений этих переменных, выбрать по одному значению из каждого множества (допустим в результате выбрали числа i1, i2, i3) и записать нечто следующее:

if
  :: var = i1;
  :: var = i2;
  :: var = i3;
fi;

Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них.

Имитирование системных вызовов

Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения.

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

01 02 03 04 05 06 07 08 09 10

Календарь

	пт	пт	пт	пт	пт
Февраль		08	15	22	29
Март		14	21	28
Апрель	04	11	18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин

Получено с 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_3

@@ Строка 64: / Строка 64: @@
 === Решение ===
+==== Модель ====
 <pre>#define OK 0
 #define NOT_OK 1
@@ Строка 159: / Строка 161: @@
 }</pre>
-=== Вывод симулирования ===
+==== Вывод симулирования ====
 [[Изображение:Screenshot-Sequence Chart.png|thumb|Cкриншот диаграммы состояний]]

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

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

Версия 10:01, 25 апреля 2008

Содержание

Задача

Вариант 1

Исходный текст функции

Свойства корректности

Решение

Модель

Вывод симулирования

Пояснения

Абстрагирование

Недетерминизм

Имитирование системных вызовов

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты