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

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

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

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

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

Пример

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

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

== Конструкция never (отрицания свойств) ==

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

Попробуем сформул. св-ва, в котором за p следует q/ dJ-GTHDS[? YF CFVJV LTKT? CKTLETN GJYZNM? XNJ PYFXBN @CKTLETN@. Если мы имеем в виду не неодновременное выполнение p и q, то первый вариант неправильный. Правмльный --- второй вариант. Нам нужно, чтобы конструкция, которая пров. наше св-во, выполнялась синхронно с моделью. Такой конструкцией является конструкция never. 
* Выполняется синхронно моделью. То есть на каждый шаг выполн. шаг never
* Если достигнут конец never, то ошибка
* ...

Пример
...

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

Gjxtve vs botv jnhbwfybt cd-d? f yt dsgjkytybt^ потому что если мы ищем выполнимость, то надо перебрать все трассы, впротивном случае надо найти одну трассу. То есть мы описываем то, чего не должно быть.

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

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

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

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

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

== Автоматы Бюхи ==

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

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

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

...

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

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

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

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

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

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

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

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

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

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

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

Просмотры

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

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 17: / Строка 17: @@
 Вводилось опред. трассы, и трасса и есть посл. наблюд. атомар. высказываний. Для программы mutex приведён пример вычисл. посл. сост. и переходов между ними и знач. перем.
-Попробуем сформул. св-ва, в котором за p следует q. Во-первых, на самом деле, следует понять, что значит "следует". Если мы имеем в виду не неодновременное выполнение p и q, то первый вариант неправильный. Правильный --- второй вариант. Нам нужно, чтобы конструкция, которая пров. наше св-во, выполнялась синхронно с моделью. Такой конструкцией является конструкция never.
+Попробуем сформул. св-ва, в котором за p следует q/ dJ-GTHDS[? YF CFVJV LTKT? CKTLETN GJYZNM? XNJ PYFXBN @CKTLETN@. Если мы имеем в виду не неодновременное выполнение p и q, то первый вариант неправильный. Правмльный --- второй вариант. Нам нужно, чтобы конструкция, которая пров. наше св-во, выполнялась синхронно с моделью. Такой конструкцией является конструкция never.
 * Выполняется синхронно моделью. То есть на каждый шаг выполн. шаг never
 * Если достигнут конец never, то ошибка
@@ Строка 25: / Строка 25: @@
 ...
-Конструкция never:
+Конмтструкция never:
 * ...
-Почему мы ищем отрицание свойств, а не выполнение? потому что если мы ищем выполнимость, то надо перебрать все трассы, впротивном случае надо найти одну трассу. То есть мы описываем то, чего не должно быть.
+Gjxtve vs botv jnhbwfybt cd-d? f yt dsgjkytybt^ потому что если мы ищем выполнимость, то надо перебрать все трассы, впротивном случае надо найти одну трассу. То есть мы описываем то, чего не должно быть.
 Из тела never можно ссылаться на точку процесса.
@@ Строка 42: / Строка 42: @@
 Если нужно сослаться за действие? Есть ассерты на трассы. Можно в ассерте задать ограничение на последовательности send и recieve, а также на каналы и отправляемые значения. Конструкция называется trace.
-Далее мы формально опишем, как с помощью формального автомата описать, что что-то невозможно и рассмотрим LTL.
+Далее мы формально опишем, как с помощью формального автомата описать, что что-то невозможно и рассмотрим LCL.
 == Автоматы Бюхи ==