ВПнМ, 09 лекция (от 11 апреля)

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: = Логика линейного времени. Исаользование LTL в Spinю Другие темпоральные логики = Сегодня мы закончим с T...)
м
 
Строка 1: Строка 1:
 +
'''Презентация:''' http://savenkov.lvk.cs.msu.su/mc/lect9.pdf<br />
 +
'''Диктофонная запись:''' http://esyr.org/lections/audio/verification_2008_summer/verification_08_04_11.ogg
 +
= Логика линейного времени. Исаользование LTL в Spinю Другие темпоральные логики =
= Логика линейного времени. Исаользование LTL в Spinю Другие темпоральные логики =

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

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

Содержание

[править] Логика линейного времени. Исаользование LTL в Spinю Другие темпоральные логики

Сегодня мы закончим с TLL, посмотрим, как верифицировать модели при помощи LTL в Spin, и поговорим о выразит. возм. LTL в сравн. в другими лдогиками.

[править] Про практикум

Ошибки и странности:

  • "Я хочу повысить вероятность." Недетерм. свзан не с понятием вероятности, а с понятием возможности. И в ходе вериф. интересуют возм. пути, а не вероятные.
  • Ожидание выполн. усл. в виде цикла. Для этого есть родные конструкции Promela.
  • Недетерм. через присвоение перем. и проверки её знач. От этого нужно просто абстрагироваться.
  • Некорректное моделир. вызова функции: вызов сьрасывается, если ядро занято
  • Построение полной модели, а потом убирание всего лишнего. Сначала надо читать спецификацию.

[править] LTL

Рассмотрели все операторы, кроме next.

[править] Оператор next

Используя этот оператор, мы формулир. предп. о том, какое сост. системы будет следующим. Если у нас линейная сист., то такое можно предп. Если же модель сост. из неск. процессов, то есть внеш. недетерм., может далее быть вып. любой процесс, и требование может оказаться слишком жёстким или невыполнимым. Стоит ограничиваться предп. о справдел. планирования.

[править] Свойства, инвариантные к прореживанию

Трассу можно записать, как посл. сост. с указ. кол-вом шагов, на которых они ывп. E(φ) --- всевозм. трассы, отл. лишь количеством шагов. E(φ) --- расширение φ.

Пример: ...

Свойства, инвар. к прореж. --- св-ва, которые выполн. либо на всех трассах на E(φ), либо ни на одной. Св-ва. зависят не от длины трассы, а от посл.,, в которой они сменяют друг друга. Доказано, что если мы выкенем из LTL оператор X, то мы сможем описать все св-ва, инвар. прореж. Такое подмн-во LTL наз. LTL-X и дост. широко исп.

  • Удобно проверять допустимость авт. Бюхи
  • Удобно опис. св-ва при помощи LTL

Следовательно, нужна связь между ними. Бе этого грустно. Однако здесь повезло, и для каждой LTL-формулы сущ. автомат Бюхи, который допускает те и только те трассы, котторые заданы формулой.

Пример: ...

Нужно помнить, что св-ва мы описываем на LTL, а проверять мы хом, чот прогр. не демонстр. непр. поведения, т. е. осн. инструмент --- конструкция never. Каким образом позитивное утв. LTL, приводится к нег. утв. never? Есть св-во, что если LTL-формула выполн. на любой трассе, то её отрицания не вып. ни на какой. След, автомат строится для отрицания исх. формулы.

Пример: ... Каким обр. мы строим этот автомат: Мы опускаем знак отр. внутр., и далее строится опзитивный, опуск. автомат, но у которого на дугах стоят операторы отриц.

Спин умеет строить констр. never на осн. LTL-формул: spin -f.

[править] Правила синтаксиса задания

  • Вводим строчные опред. для всех булевых формул
  • Следим за проиритетом
  • Spin очень плохо умеет минимизировать формулы. Существуют сторонние утилиты, которые входят в дистр., но необх. при написании практ. не возн.

[править] Отрицание LTL-формул

LTL-формулу всегда можно преобр. так, что отр. будут только перед прооз. ворм.

[править] Использование LTL для проверки правильности в Spin

  • Булевы формулы --- пропоз.
  • Проверяем отрицание условий
  • Дописываем сгенер. модель

Существует много рес-в про то, как форм. св-ва на LTL. Есть ряд проэктов, этому посвящ.

Паттерны делятся нв паттерны встречаемости и порядка. Встречаемость делится на остутств., сущ. и униврес., порядок делится на приоритет и отклик.

[править] Выраз. мощность LTL по ср. с never

  • never экв. автоматам Бюхи, к-рые опис. ω-рег. язык
  • LTL опис. подмн-во. Но добавление квантора сущ. надо одним пропоз. символов. делает LTL эквив. по мощн.

Сущ-вуют утилиты, которые позв. преобр. такой расшир. LTL в Promela.

[править] Сравнение LTL с другими логиками

  • LTL
  • CTL* --- логика ветвящегося времени
  • CTL --- фрагмент CTL*


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы