Уточнение абстракции на основе контрпримеров

Уточнение абстракции на основе контрпримеров (CEGAR) — это метод символьной проверки модели . Он также применяется в модальной логики алгоритмах табличных исчислений для оптимизации их эффективности.

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

Если желаемое свойство программы не удовлетворяется абстрактной моделью, генерируется контрпример. Затем процесс CEGAR проверяет, является ли контрпример ложным, т. е. применим ли контрпример также к недоабстракции, но не к реальной программе. Если это так, то делается вывод, что контрпример объясняется недостаточной точностью абстракции. В противном случае процесс обнаруживает ошибку в программе. Уточнение выполняется, когда контрпример оказывается ложным. Итеративная процедура завершается либо в случае обнаружения ошибки, либо когда абстракция уточняется до степени, эквивалентной исходной модели.

Проверка программы

Абстракция

Смотрите также: структура Крипке

Чтобы рассуждать о правильности программы, особенно тех, которые включают концепцию времени для параллелизма , используются модели перехода состояний. В частности, модели с конечным состоянием могут использоваться вместе с темпоральной логикой при автоматической проверке. Таким образом, концепция абстракции основана на сопоставлении двух структур Крипке . В частности, программы могут быть описаны с помощью автоматов потока управления (CFA).

Определите структуру Крипке $M$ как $\langle S,s_{0},R,L\rangle$, где

• $S$ представляет собой конечное множество состояний,
• $s_{0}$ является начальным состоянием в $S$,
• $R$ является полным переходным отношением, и
• $L$ — это функция, которая помечает каждое состояние набором пропозициональных имен, которые в нем содержатся.

Абстракция $M$ определяется $\langle S_{\alpha },s_{0}^{\alpha },R_{\alpha },L_{\alpha }\rangle$ где $\alpha$ — это отображение абстракции, которое отображает каждое состояние в $S$ в государство в $S_{\alpha }$.

Чтобы сохранить критические свойства модели, отображение абстракции отображает начальное состояние исходной модели. $s_{0}$ своему коллеге $s_{0}^{\alpha }$ в абстрактной модели. Отображение абстракции также гарантирует сохранение переходных отношений между двумя состояниями.

Проверка модели

На каждой итерации проверка модели выполняется для абстрактной модели. Например, проверка ограниченной модели генерирует пропозициональную формулу, которая затем проверяется на логическую выполнимость решателем SAT .

Уточнение

Когда обнаруживаются контрпримеры, их исследуют, чтобы определить, являются ли они ложными примерами, т. е. не являются ли они недостоверными примерами, возникающими из-за недостаточной абстракции модели. Неложный контрпример отражает некорректность программы, чего может быть достаточно, чтобы прекратить процесс проверки программы и сделать вывод о ее некорректности. Основная цель процесса уточнения — обработка ложных контрпримеров. Он устраняет их за счет увеличения детализации абстракции.

Процесс уточнения гарантирует, что тупиковые и плохие состояния не принадлежат одному и тому же абстрактному состоянию. Тупиковое состояние — это достижимое состояние без исходящего перехода, тогда как плохое состояние — это состояние, в котором переходы вызывают противоположный пример.

Таблица расчета

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