Редактирование: ВПнМ, 03 лекция (от 22 февраля)

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

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

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

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

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

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

Необходимое свойство: множество AP<sub>&phi;</sub> должно включаться в AP<sub>m</sub>

Есть два предиката, 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, который вып. один раз. В промела также поддерживаются типичные операторы в циклах.

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

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_03_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_22_%D1%84%D0%B5%D0%B2%D1%80%D0%B0%D0%BB%D1%8F%29

Редактирование: ВПнМ, 03 лекция (от 22 февраля)

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

Просмотры

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

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 5: / Строка 5: @@
 = Система верификация Spin =
-Сейчас будем говорить про возможности моделирования без учёта возможностей верификации.
+Сейчас будем говорить про возможности моделирования без учёта возмосностей верификации.
 Без определения на прошлой лекции осталось свойство адекватности.
@@ Строка 17: / Строка 17: @@
 * Первая адекватна, вторая --- нет. Получаем контрпример. На модели свойство не выполняется, на программе -- выполняется. Мы потеряли завершаемость с петлёй. Тем самым, вторая модель неадекватна. Как мы это выяснили: получили контрпример, проверили на исходной системе, выяснили. А если на модели свойство будет выполняться, а на системе --- нет? Такого быть не может, поскольку все пути на системе отображаются на модель.
-== Верификация моделей в среде SPIN ==
+== Верифик. моделей в среде SPIN ==
-Когда мы верифицируем программу, мы хотим описывать, как система устроена и как она должна быть устроена. Соответственно, нам нужна нотация для описания поведения и требований.
+кОГДА МЫ ВЕРИФ. ПРОГРАММУ, МЫ хОТИМ ОПИСЫВАТЬ, как система устроена, другая, как она должна быть устроена. Соотв., нам нужна нотация для описания повед. и требований.
 Первое: верификатор:
-* Устройство системы удовлетворяющее свойствам правильности
+* Устройство системы удовл. св-вам правильности
 * Выбранная нотация гарантирует разрешимость проверки любого свойства