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

Оригинальная презентация: http://savenkov.lvk.cs.msu.su/mc/lect3.pdf

Задания могут сдаваться по почте, на семинарах будет сдаваться то, что явно сказано.

Система верификация Spin

Сейчас будем говорить про возможности моделирования без учёта возможностей верификации.

Без определения на прошлой лекции осталось свойство адекватности.

Необходимое свойство: множество AP_φ должно включаться в AP_m

Есть два предиката, p и q, хотим рассмотрим только q, оставляем только его, потом объединяем два одинаковых состояния. Посмотрим, для каких свойств они будут адекватны:

• Нет, так как не наблюдаем p
• Обе модели адекватны
• Первая адекватна, вторая --- нет. Получаем контрпример. На модели свойство не выполняется, на программе -- выполняется. Мы потеряли завершаемость с петлёй. Тем самым, вторая модель неадекватна. Как мы это выяснили: получили контрпример, проверили на исходной системе, выяснили. А если на модели свойство будет выполняться, а на системе --- нет? Такого быть не может, поскольку все пути на системе отображаются на модель.

Верификация моделей в среде SPIN

Когда мы верифицируем программу, мы хотим описывать, как система устроена, другая, как она должна быть устроена. Соотв., нам нужна нотация для описания поведения и требований.

Первое: верификатор:

• Устройство системы удовлетворяющее свойствам правильности
• Выбранная нотация гарантирует разрешимость проверки любого свойства

Грубо: описываем правильное поведение, описываем неправильное, описываем, что есть, и пересеч. что есть с непр. должно быть пустым.

... Spin, Promels, LTL ...

В задаче Spin как прогр. средству вменяется вериф. программы и моделирование. Моделир. может исп. для того как система работает и для проверки контрпримеров.

Promela --- язык с охраняемыми командами. Дейкстра придумал язык, в котором на кадждый оператор навешивается страж, вот это оно.

• Язык позв. писать плохой код. в этом смысле он хороший.

Процесс верификации

Ключевые моменты

• У млодели конеч. число сост. --- гарантирует конечность верификации.
• Процессы выполняются асинхронно, нет глобальных часов, синхронизация отсут.
• У отдельного процесса может быть недетерм. поток управл.
• Понятие выполнимости оператора. С любым оператором связано предусловие, оператор выполн., когда предусл. выполнено. Пример: q?m --- чтение m из канала q.

Устройство модели

Есть процессы, еслть глобальные и локальные объекты данны

Хелловорлд

Естественно начать изучение программы с хелловорлд. Язык очень похож на С.

active --- тип процесса --- инстанцируется немедленно

main --- произвольное имя процесса

--- разделитель команд

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

Пример --- процесс, который создаёт 2 свои копии. Несмотря на реурсию, эта система остаётся конечной. Максимальное число процессов ограничено 255.

Пример на оператор run --- процесс выводит свой номер, init создаёт два процесса и говорит об этом. Тут стоит обратить внимание на предопр. переменных, а также на то, что печать и присв. происх. всегнда, а запуск тодлько тогда, когда можно.

Два способа взаимодействия --- shmem и обмен сообщениями. У каждого процесса есть локальное сост. У модели вцелом есть глобальное состояние.

Почему число сост. конечно --- конеч. кол-во процессов, огр. количество операторов, ограниченные типы данных, огр. размер каналов. --- задача вериф. разрешима.

Как можно синхр. процессы между собой: самое простое --- явняа синхронизация. Ошибка в первой строчке B() --- должно быть cnt--

Основные операторы Promela

Операторы задают элем. преобр. сост. процессов и этими операторами размеч. дуги в системе переходов. Оператор может быть выполнимым или заблокированным, выполнимость может зависеть от глоб. сост. системы.

В примерах уже встреч неск. типов операторов:

• Печать. Выполн. всегда, не влияет ни на что
• Оператор присваивания. Выполн. Всегда, меняет левую часть
• Оператор-выраж --- выполним, только если выражение не равно 0.

Примеры выражений: ...

Смысл выполнения выражения: выражение --- осн. мех. синхр., осн. мех управления процессами, соответственно, мы записываем выражение, и, если знач. равно нулю, то осн. вып. процесса. Это тот самый страж Дейкстры.

Как говорилось, процессы вып. асинхронно. Между выполн. двух посл операторов может пройти сколько угодно времени, и в это время могут быть выполн. операторы других процессов. Если мы хотим установить порядок вып., то должны установить его явно.Операторы выполн. атомарно. Также есть ср-ва атомарного выполнения цепочки операторов. В теле одного процесса также допускается недетерм. ветвление.

В промеле: два вида недетерминизма, внеш. и внутр

• Ндетерм. выбор процесса
• Недетерм. выбор действия

Пример внешнего недетерминизма: ...

Выполнимость операторов

Осн мех. упр. вып. операторов --- выражения, они активно исп. Вместо пустых циклов ожидания активно используются стражи. В примере ошибка --- наоборот.

Псевдо-операторы

• Может встречаться в выражениях

Ещё есть тип оператора --- ассерт, соответствует ассертам в С. Не влияет на состояние. Если выражение внутри ассерта не равно 0, то ошибка.

В примере ассерт может быть выполнен в любой момент, что соотв. инварианту.

Пример: типичный мех. синхр. с другим процессом.

Оператор рун

Все другие операторы не приводят к побоч. эфф., оператор рун приводит к порожд. процесса.

• если run (B and run a()) --- процесс будет заблокирован, но процесс буден создан
• Если оператор run возвр 0, то это наверняка ошибка.

- Как оценивается задание? - Как балет --- сидят 5 человек, оценивают от 0 до 6... - Zerocool: Zero, zero, zero, ... - Ну, это не у меня ник Zerocool...

Пример с 2 процессами

В promela есть перечислимый тип, он практически такой же, как enum в С.

Если перем не иниц, то это довольно быстро выплывет.

do...od задаёт беск. цикл.

При помощи :: задаётся посл. вариантов. Если выполнимо выражение, след за ::, то посл. выполн. все операторы в одной посл. Таких посл. могут быть несколько. Если вып. стражи в неск. посл, то выбор ветки будет недетерм.

Соответственно, здесь есть два процесса. Есть producer и consumer.

Эти процессы могут вып. сколь угодно долго, но мы задаём ключ с числом шагов.

If

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

То, что связано с каналами сообщ, будет на след. лекции. Это каналы Петерсона, это будет доло и мучительно.