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

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

презентация: http://savenkov.lvk.cs.msu.su/mc/lect7.pdf
Диктофонная запись: http://esyr.org/lections/audio/verification_2008_summer/verification_08_03_28.ogg

Пример

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

[править] Свойства правильности

Свойства формулируются через assert,также программа эффективно работает, пока увел. зн. максимум. Разметив меткой прогресс, видим, что рпограмма рабьотает эффективно.

[править] Конструкция never (отрицания свойств)

Вспомним, как констр. св-в описываются на посл. сост. Мы можем опр. св-во:

• Как посл. сост.
• Как посл. переходов
• Как посл. знач. в этих сост.

Вводилось опред. трассы, и трасса и есть посл. наблюд. атомар. высказываний. Для программы mutex приведён пример вычисл. посл. сост. и переходов между ними и знач. перем.

Попробуем сформул. св-ва, в котором за p следует q. Во-первых, на самом деле, следует понять, что значит "следует". Если мы имеем в виду не неодновременное выполнение p и q, то первый вариант неправильный. Правильный --- второй вариант. Нам нужно, чтобы конструкция, которая пров. наше св-во, выполнялась синхронно с моделью. Такой конструкцией является конструкция never.

• Выполняется синхронно моделью. То есть на каждый шаг выполн. шаг never
• Если достигнут конец never, то ошибка
• ...

Пример ...

Конструкция never:

• ...

Почему мы ищем отрицание свойств, а не выполнение? потому что если мы ищем выполнимость, то надо перебрать все трассы, впротивном случае надо найти одну трассу. То есть мы описываем то, чего не должно быть.

Из тела never можно ссылаться на точку процесса.

Прммеры исп.:

• Нахождение неск. процессов в крит. секции
• Проверка, не завершился ли процесс

Видимость

• Конструкции never --- глобальны
• Как следствие, можно ссылаться на всё, кроме локальных переменных и действий

Если нужно сослаться за действие? Есть ассерты на трассы. Можно в ассерте задать ограничение на последовательности send и recieve, а также на каналы и отправляемые значения. Конструкция называется trace.

Далее мы формально опишем, как с помощью формального автомата описать, что что-то невозможно и рассмотрим LTL.

[править] Автоматы Бюхи

• Свойство выполн. на модели, если оно выполняется на любой трассе
• Свойство нарушается, если сущ. хотя бы одна трасса, на которой это не так

Один важный момент: док. нарушения отлич. от док. выполнения. противоп. св-ва.

Проще проверять наруш., чем вып.

...

Проходом автомата назыв. упорядоч. мн-во его переходов. У нас есть проход как послед. переходов. Этому проходу соотв. послед. сост., послед. меток. Допускающим. назыв. проход, останав. в терм. сост. Языком автомата наз. множество слов, соотв. допускающим проходам автомата.

Пример: свойство можно описать ДКА.

Иногда нужно рассуждать о беск. задержке. Это легко описать автоматом, но языком --- нет, т. к. слова конечной длины. В этом случае надо расширить понятие допустимости: бесконечный проход состоит из коечного префикса и беск. суффикса. Мыр азделяем проходы на две части. Беск. повт. часть мы обозн. чсимвлолом ω. После этого вводится конеч. автомат с опр. допуск. прохода по Бюхи (ω-допускание). То есть, мы вып. префикс, и бальше беск. часто будем попадать в терм. сост.

Эта теория хорошая, но она не учитывает конечные проходы, и хорошо бы эти бва вариант объединить. Это делается расширением путём введения долон. символа ε, и в конечных прохожах в конце беск. эпсилон. Т. о., автомат Б. подходит для опис. конеч. и беск. св-в. Всё хорошо. Осталось только научиться опред. свойства на логике LTL, и можно будет проверить при помощи спина всё, что угодно.