ВПнМ, 09 лекция (от 11 апреля)
Материал из eSyr's wiki.
ESyr01 (Обсуждение | вклад)
(Новая: = Логика линейного времени. Исаользование LTL в Spinю Другие темпоральные логики = Сегодня мы закончим с T...)
К следующему изменению →
Версия 12:07, 11 апреля 2008
Содержание |
Логика линейного времени. Исаользование 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*
Верификация программ на моделях
Календарь
пт | пт | пт | пт | пт | |
Февраль
| 08 | 15 | 22 | 29 | |
Март
| 14 | 21 | 28 | ||
Апрель
| 04 | 11 | 18 |
Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин