2.7.2. Формальная верификация
Формальная верификация касается формального доказательства корректности системы с использованием языка математики. Первое что требуется это построение формальной модели. Этот шаг трудно автоматизировать, и требует некоторых усилий. Получив модель можно попытаться доказать определенные свойства.
Техники формальной верификации могут быть классифицированы по типу используемой логики.
Логика высказываний (пропозициональная логика). В этом случае модели состоят из булевых функций, а соответствующие инструменты называют Булевой проверкой, проверкой на тавтологию или проверкой на эквивалентность. Они могут быть использованы для проверки того что два представления булевых функций (или множества булевых функций) эквивалентны. На сегодня логика высказываний разрешима, она также разрешима независимо от того эквивалентны или нет два представления (нет сомнительных случаев). Например, одно представление может соответствовать вентилям реальной схемы, а другое спецификации. Доказательство затем эквивалентности доказывает, что результат всех преобразований (например, оптимизация энергопотребления или задержки) проекта являются корректными. Булева проверка может справиться с очень большими проектами с такими, как и исчерпывающая валидациия, основанная на моделировании. Ключевая причина мощи Булевой проверки заключается в использовании бинарного дерева решений (BDD). Сложность задачи проверки на эквивалентность булевых функций представленных BDD является линейной от числа узлов BDD. Напротив сложность задачи проверки на эквивалентность булевых функций представленных суммой произведений является NP-полной. Основанная на BDD проверка на эквивалентность по этой причине заменила симуляторы и работает со схемами из миллионов транзисторов.
Логика первого порядка (FOL). FOL включает операторы ∃ и ∀. Обычно допускаются также целые числа. Некоторая автоматизация для проверки FOL выполнима. Однако на сегодня FOL неразрешима. Это означает, что могут быть неопределенные случаи. Популярной техникой является исчисление Хоара (Hoare).
Логика высшего порядка (HOL). HOL базируется на лямбда-исчислении и позволяет манипулировать функциями так же как другими объектами. Для HOL доказательства едва ли когда-нибудь удастся автоматизировать и обычно должно выполняться вручную с некоторой поддержкой доказательства.
Логика высказываний может быть использована для проверки комбинационных логических схем. Она не может напрямую моделировать конечные автоматы. Для конечных автоматов необходимо оборвать обратные связи в схеме FSM и работать с несколькими копиями FSM, каждая из которых представляет результат воздействия одного входного набора (итерационная модель автомата с памятью). Однако этот метод не работает для длинных входных последовательностей.
С такими последовательностями может справиться техника «проверка модели» (model checking). Обычно проверка модели применялась для проектирования аппаратуры, но в последние 10-15 лет используется при разработке ПО. Эта техника использует темпоральную логику для задания спецификации, т.к. последняя способна выражать требования по безопасности для одновременных систем. Темпоральная логика является разновидностью модальной логики. Она изначально разрабатывалась для выражения таких модальностей как необходимость и возможность.
Темпоральная логика используется для рассуждения о знании, позволении, обязательстве.… Для текущего состояния она рассуждает о том, что есть истина на основании истинности или лжи атомарных высказываний. Она рассматривает выполнение системы как последовательность состояний, когда «текущее время» является индексом в последовательности. Будущее – более поздний индекс, прошлое – более ранний индекс.
Синтаксис темпоральной логики состоит из:
• p: примитивные высказывания;
• стандартные булевы связки (¬, ∨, ∧, ⇒);
• темпоральные операторы:
• Gφ φ всегда истинно (т.е. теперь и в будущем), глобально;
• Fφ φ истинно когда-нибудь в будущем;
• Xφ φ истинно в следующий момент времени;
• φUψ φ истинно пока не ψ истинно;
Задача проверки модели:
Пусть M граф переходов.
Пусть φ спецификация в темпоральной логике (темпоральная формула).
Найти все состояния s графа переходов M такие, что M, s⊨ φ.
В качестве примера рассмотрим микроволновую печь [35]. На рис. 92 приведена модель вычислений микроволновой печи в виде графа переходов M. Модель содержит четыре атомарных высказывания:
• Start: нажата кнопка – “start”;
• Close: дверца закрыта?;
• Heat: печь активна;
• Error: состояние ошибки.
Рис. 92. Граф переходов микроволновой печи
Состояния графа представляют ситуации (различные комбинации из атомарных высказываний), в которых может находиться система в различные моменты времени. Ребра могут иметь метки изображающие действия системы.
Рассмотрим свойство безопасности (спецификация), которое на естественном языке формулируется следующим образом: печь не нагревается, пока не закрыта дверь. Это свойство в виде темпоральной формулы имеет вид: (¬Heat) U Close. На рис. 93 приведено решение задачи проверки модели для микроволновой печи на соответствие свойству безопасности. Во всех состояниях свойство подтверждается.
Рис. 93. Проверка свойство безопасности микроволновой печи
Инструмент верификации, использующий технику проверки модели, имеет два входа:
•модель, которую необходимо проверить;
• свойства, которые требуется проверить.
Инструмент верификации может доказать или опровергнуть свойства. В последнем случае он может предоставить контр пример (последовательность действий системы, на которой нарушается спецификация). Проверка модели легче автоматизируется, чем FOL.
EMC-система [36] интегрирует проверку модели и логику высшего порядка (рис. 94).
Рис. 94. EMC-система
Эта система принимает свойства, описанные как CTL формулы (Computation tree logic – логика вычислительного дерева). CTL формулы состоят из двух частей:
– квалификатор пути специфицирует пути в графе переходов;
– квалификатор состояния специфицирует состояния.
Например, M, s |= AGg означает, что в графе переходов M свойство g сохраняется для всех путей (обозначены как A), начинающихся в s и всех состояний (обозначены как G).