Введение

Область информатики – проверка моделей

В информатике проверка моделей, или проверка свойств, – это метод определения, удовлетворяет ли модель системы с конечным числом состояний заданной спецификации (также известной как требование к корректности). Обычно это применяется к аппаратным или программным системам, где спецификация включает требования живучести (например, предотвращение взаимной блокировки) и требования безопасности (например, предотвращение состояний, представляющих сбой системы). Для алгоритмического решения такой задачи как модель системы, так и её спецификация формализуются на некотором точном математическом языке. В связи с этим задача формулируется как задача логики, а именно – проверка, удовлетворяет ли структура заданной логической формуле. Эта общая концепция применима ко многим видам логики и структурам. Простая задача проверки модели заключается в проверке, удовлетворяет ли формула в пропозициональной логике заданной структуре.

Обзор

Проверка свойств используется для верификации, когда два описания не эквивалентны. В процессе уточнения спецификация дополняется деталями, которые не требуются в спецификации более высокого уровня. Нет необходимости проверять вновь введенные свойства относительно исходной спецификации, поскольку это невозможно. Поэтому строгая проверка двунаправленной эквивалентности заменяется на однонаправленную проверку свойств. Реализация или проект рассматривается как модель системы, а спецификации – как свойства, которым должна удовлетворять модель. Был разработан важный класс методов проверки моделей для верификации моделей аппаратных и программных разработок, где спецификация задается формулой темпоральной логики. Пионерскую работу в области спецификации темпоральной логики выполнил Амир Пнуэли, удостоенный премии Тьюринга в 1996 году за "фундаментальный вклад в применение темпоральной логики в информатике". Проверка моделей началась с новаторских работ Э. М. Кларка, Э. А. Эмерсона, Ж.-П. Квейля и Ж. Сифакиса. Кларк, Эмерсон и Сифакис разделили премию Тьюринга в 2007 году за их основополагающий вклад в создание и развитие области проверки моделей. Проверка моделей чаще всего применяется к аппаратным разработкам. Для программного обеспечения, из-за неразрешимости (см. теорию вычислимости), подход не может быть полностью алгоритмическим, применим ко всем системам и всегда давать ответ; в общем случае, он может не доказать или опровергнуть заданное свойство. В аппаратном обеспечении встраиваемых систем возможно валидировать спецификацию, представленную, например, с помощью диаграмм деятельности UML или интерпретируемых сетей Петри. Структура обычно задается в виде описания исходного кода на промышленном языке описания аппаратуры или языке специального назначения. Такая программа соответствует конечному автомату (FSM), то есть ориентированному графу, состоящему из узлов (или вершин) и ребер. С каждым узлом связан набор атомарных высказываний, обычно указывающих, какие элементы памяти находятся в состоянии "один". Узлы представляют состояния системы, ребра – возможные переходы, которые могут изменить состояние, а атомарные высказывания – базовые свойства, выполняющиеся в точке исполнения. Формально, задача может быть сформулирована следующим образом: дано желаемое свойство, выраженное формулой темпоральной логики, и структура с начальным состоянием, определить, выполняется ли. Если структура конечна, как это обычно бывает в аппаратном обеспечении, проверка моделей сводится к поиску в графе.

Проверка символической модели

Вместо перечисления достижимых состояний по одному, пространство состояний иногда можно более эффективно исследовать, рассматривая большое количество состояний за один шаг. Когда такое исследование пространства состояний основано на представлении множества состояний и переходов в виде логических формул, бинарных диаграмм решений (BDD) или других связанных структур данных, метод проверки моделей называется символическим. Исторически, первые символические методы использовали BDD. После успеха решателей задачи выполнимости булевых формул (SAT) в решении задачи планирования в искусственном интеллекте (см. Satplan) в 1996 году, этот же подход был обобщен для проверки моделей в линейной временной логике (LTL): задача планирования соответствует проверке модели на свойства безопасности. Этот метод известен как ограниченная проверка моделей. Успех решателей SAT в ограниченной проверке моделей привел к их широкому использованию в символической проверке моделей.

Техника

Инструменты проверки моделей сталкиваются с комбинаторным взрывом пространства состояний, общеизвестным как проблема взрыва состояний, которую необходимо решить для решения большинства практических задач. Существует несколько подходов к преодолению этой проблемы. Символические алгоритмы избегают явного построения графа для конечных автоматов (FSM); вместо этого они представляют граф неявно, используя формулу в квантифицированной пропозициональной логике. Использование бинарных диаграмм решений (BDD) получило распространение благодаря работам Кена Макмиллана, а также Оливье Кудера и Жана Кристофа Мадре, и разработке библиотек манипулирования BDD с открытым исходным кодом, таких как CUDD и BuDDy. Алгоритмы ограниченной проверки моделей разворачивают FSM на фиксированное число шагов, *n*, и проверяют, может ли нарушение свойства произойти за *n* или меньше шагов. Обычно это включает кодирование упрощенной модели в виде экземпляра SAT. Процесс может повторяться с увеличением *n* до тех пор, пока не будут исключены все возможные нарушения (ср. поиск в глубину с итеративным углублением). Абстракция пытается доказать свойства системы, сначала упростив её. Упрощенная система обычно не удовлетворяет точно тем же свойствам, что и исходная, поэтому может потребоваться процесс уточнения. Как правило, требуется, чтобы абстракция была корректной (свойства, доказанные для абстракции, верны для исходной системы); однако иногда абстракция не является полной (не все истинные свойства исходной системы верны для абстракции). Примером абстракции является игнорирование значений небулевых переменных и рассмотрение только булевых переменных и потока управления программой; такая абстракция, хотя и может показаться грубой, на самом деле может быть достаточной для доказательства, например, свойств взаимного исключения. Абстракция, управляемая контрпримерами (CEGAR), начинает проверку с грубой (т.е. неточной) абстракции и итеративно её уточняет. Когда обнаруживается нарушение (т.е. контрпример), инструмент анализирует его на предмет реализуемости (т.е. является ли нарушение подлинным или результатом неполной абстракции?). Если нарушение реализуемо, оно сообщается пользователю. Если нет, то доказательство нереализуемости используется для уточнения абстракции, и проверка начинается заново. Инструменты проверки моделей изначально разрабатывались для рассуждений о логической корректности систем дискретных состояний, но впоследствии были расширены для работы с системами реального времени и ограниченными формами гибридных систем.

Логика первого порядка

Проверка моделей также изучается в области теории вычислительной сложности. В частности, фиксируется формула логики первого порядка без свободных переменных и рассматривается следующая задача принятия решения:

Для данной конечной интерпретации, например, представленной в виде реляционной базы данных, определить, является ли эта интерпретация моделью формулы. Эта задача принадлежит классу AC0. Она становится разрешимой при наложении определенных ограничений на входную структуру: например, требовании, чтобы ширина ее дерева была ограничена константой (что в более общем случае подразумевает разрешимость задачи проверки моделей для монадической логики второго порядка), ограничении степени каждого элемента области определения, а также более общих условиях, таких как ограниченное расширение, локально ограниченное расширение и структуры, нигде не плотные. Эти результаты были расширены на задачу перечисления всех решений формулы первого порядка со свободными переменными.