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

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

Презентация: 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. Есть ряд проэктов, этому посвящ.

• http://patterns.projects.cis.ksu.edu

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

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

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

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

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

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