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

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

Текущая версия

Диктофонная запись: 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, она будет вызывать другие системные функции, и будет дано свойство, которое нужно проверить. Нужно построить модель системы, которая будет сохранять свойства, и функции будут взаимод. через передачу сообщений. После модели нужно свойства проверить. Для этого нужно их строго задать в системе спин, а как это делать, будет рассказано далее. Дедлайны для моделирования и вериф. будут разные. Дедлайн будет указан в письме, примерно это будет две недели на моделирование и неделю на верификацию. Данные никакие вычылать не надо. Эту задачу на экзамене будет сделать чрезвычайно сложно.