Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 90 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 983: | Строка 983: | ||
=== Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. === | === Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. === | ||
- | * Свойство ''выполняется'' на модели, если оно выполняется на всех трассах. | ||
- | * Свойство ''нарушается'' на модели, если нарушается хотя бы на одной из трасс. | ||
- | * '''Принцип верификации нарушения свойств''' - проще проверять нарушение свойства, чем выполнение свойства. | ||
- | ** Достаточно найти один контрпример | ||
- | * Нарушение свойства описывается при помощи конструкции never – автомата, распознающего неправильное поведение | ||
- | ** Автоматы Бюхи | ||
- | * Свойства на последовательностях состояний удобно описывать при помощи темпоральной логики | ||
- | ** Логика LTL | ||
- | |||
- | * <u>Связь LTL с автоматами Бюхи</u> | ||
- | ** При помощи автомата Бюхи удобно проверять допустимость трасс. | ||
- | ** При помощи темпоральных формул удобно описывать свойства правильности. | ||
- | ** Для всякой LTL-формулы f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f | ||
- | * <u>Переход от LTL к автоматам</u> | ||
- | ** f выполняется на всех вычислениях <=> | ||
- | ** !f не выполняется ни на одном вычислении <=> | ||
- | ** автомат never {!f} не допускает ни одного прогона, полученного в результате синхронного выполнения с системой | ||
- | |||
- | '''Использование LTL в Spin''' | ||
- | * SPIN как раз и занимается тем, что преобразует LTL-формулы в автомат Бюхи, описываемый конструкцией never. | ||
- | * Если во время верификации нашлась трасса, принадлежащая языку автомата Бюхи (т.е, конструкция never выполнилась, и мы дошли до её конца), SPIN выдаст '''контрпример''', содержащий эту трассу. | ||
== Система Spin и язык Promela == | == Система Spin и язык Promela == |