ВПнМ, 05 лекция (от 14 марта)

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

Версия от 20:15, 23 марта 2008; ESyr01 (Обсуждение | вклад)
(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

Диктофонная запись: http://esyr.org/lections/audio/verification_2008_summer/verification_08_03_14.ogg

Вторая задача: спин не позволдяет автоматически перебрать все значения переменной, можно вручную, можно разбить на классы эквивалентности и ручками посчитать, но это необязательно, достаточно посчитать для конкретных значений переменных

Содержание

[править] Пример. Alternating Bit Protocol

  • Есть отправитель и получатель
  • Отправитель хочет убедиться в доставке сообщения, поэтому посылает дополнительный бит, который получатель должен вернуть
  • Если бит вернули, то всё хорошо, иначе повторяется посылка

(модель на Promela)

Единственный момент, который здесь выглядит, диаграмма взаимодействия, выглядит примерно так: ...

Действия по сохранению и игн. сообще здесь не присутствуют, ибо это модель. Елинственный момент --- eval, мы его рассмотрим.

Далее моделируем первые 20 шагов.

Если запустить xspin, то помимо всего прочего, можно будет увидеть диагармму взаимодействия процессов. Сейчас она неинтресна, но при выполнении следующих заданий она пригодится.

[править] Функция eval()

Основная идея этой функции --- отображаем некое значение наконстану, и используем это как ограничитель. В этом случае, приёма не будет, пока ограничитель не выполнится.

[править] Графы программ

Когда строим модель, работаем не с системой переходов, работаем с моделью, система переходов есть, но мы её не рассм. на этом этапе. И, чтобы описать сист. переходов (?), нужно хадать ... , после чего можно сформулировать свойство корректной абстракции.

Напоминание: система переходов задаёт граф, где вершины --- состояния, рёбра --- переходы.

Формально система переходов задаётся следующей сигнатурой: ...

[править] Вспомогательные определения

  • D_p --- единый абстрактный домен данных в нашей программе
  • P --- программа, эта программа определена, описана на нек-ром множестве переменных
  • ...
  • ...
  • Cond(V_p) --- набор булевых условий V_p

[править] Графы программ

Такой граф можно построить практически для любой импер. программы.

[править] Пример

Такое представление помогает избавиться от синтаксического сахара. Если возьмём программу на промеле, то переходы по метке, while, do, то они будут представлены более-менее унифицированно.

[править] Переход от PG к TS

Далее надо определить, как мы от графа перейдём к системе переходов.

  • Основная идея --- раскрутка

Это достаточно формально определение, но не достаточно строгое. Строго это делается через правила вывода.

[править] Параллелизм

[править] Интерливинг

  • Абстрагируемся от того, что у нас программа из нескольких процессов
  • Есть один процессор и несколько независимых процессов
  • Порядок выполнения процессов произволен
  • Обоснование чередования: если есть два действия, которые независимо изм. сост. программы, то их параллельное применение равносильно посл. применению в произвю порядке

[править] Пример

x = x + 1 ||| y = y - 2

В каком бы порядке мы их не выполняли, результат будет одинаков

[править] Чередование систем переходов

[править] Чередование графов программ

Если общих переменных нет, то TS(PG_1) ||| TS(PG_2) достоверно описывает композицию двух программ.

Если переменная общая есть, то получим полную лажу, следовательно, надо как-то по-другому описывать.

...

Если мы будем следовать этим правилам, то получим более достоверную систему переходов. Можно заметить, что TS(PG_!) ||| TS(PG_@) != TS(PG_1 ||| PG_2)

[править] Параллелизм и рандеву

Если расм. программы, вып. на нескольких системах, общих перпеменных там нет, надо предложить другие механизмы. Есть предача сообщений. Синхронная (рандеву, хэндшейкинг) и асинхронная (каналы сообщений). В спине, если ёмкость канала равна 0, то это синхр. передача, иначе асинхр.

[править] Рандеву

Пример рандеву: ...

Чтобы можно было удобно записывать попарную композицию, определим попарное рандеву: ...

Вторую задачку ещё можно недельку поприсылать. Третья задача: будет прислана системная функция minix, она будет вызывать другие системные функции, и будет дано свойство, которое нужно проверить. Нужно построить модель системы, которая будет сохранять свойства, и функции будут взаимод. через передачу сообщений. После модели нужно свойства проверить. Для этого нужно их строго задать в системе спин, а как это делать, будет рассказано далее. Дедлайны для моделирования и вериф. будут разные. Дедлайн будет указан в письме, примерно это будет две недели на моделирование и неделю на верификацию. Данные никакие вычылать не надо. Эту задачу на экзамене будет сделать чрезвычайно сложно.


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


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 | Теормин


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы