В.С. Буренков, С.Р. Иванов
4
Существуют инструментальные средства верификации (напри-
мер, Spin, Murphi), предоставляющие пользователю язык описания
моделей и возможность выражения условий корректности. По описа-
нию модели инструменты автоматически строят систему переходов и
проводят проверку выполнимости на ней заданной темпоральной
формулы. Указанные средства применяются для верификации про-
мышленных протоколов когерентности памяти, и хорошо себя заре-
комендовали [5–8]. Однако при этом имеется ограничение на число
узлов процессорной системы (процессорных ядер), отраженных в
модели. В [5, 7] этот параметр ограничивается значением 3–4. Более
того, современные протоколы когерентности настолько сложны, что
зачастую невозможна даже верификация систем с тремя процессора-
ми [9]. Таким образом, model checking в чистом виде не масштабиру-
ется и непригоден для параметризованной верификации.
В связи с этим применяются методы, позволяющие сократить ко-
личество состояний верифицируемой модели и в то же время сохра-
нить интересующие нас свойства исходной модели. Наиболее общи-
ми являются методы абстракции (наряду с редукцией на основе сим-
метрии и редукцией частичных порядков).
Пути получения абстрактного пространства состояний могут
быть разделены на методы аппроксимации снизу (under-approxima-
tion), удаляющие часть поведений, и методы аппроксимации сверху
(over-approximation), добавляющие новые поведения. В итоге в слу-
чае аппроксимации снизу ошибка в абстрактной системе будет под-
разумевать ошибку в исходной системе, а в случае аппроксимации
сверху корректность абстрактной системы подразумевает коррект-
ность исходной системы. В дальнейшем будут затрагиваться только
аппроксимации сверху.
Связь модели с ее абстракцией выполняет отношение симуляции
[4]. Поскольку абстракция позволяет скрыть некоторые особенности
первоначальной модели, она может быть определена на более узком
множестве атомарных высказываний. Симуляция гарантирует, что
всякое поведение в исходной модели является также поведением в ее
абстракции. Однако абстракция при этом может иметь поведения,
которые невозможны в исходной модели.
Построение абстрактных моделей требует нахождения компро-
мисса между двумя конфликтующими целями:
• получение абстрактных моделей небольшого размера, которые
могут быть верифицированы методом model checking;
• получение точных абстрактных моделей.
Чем меньше модель, тем больше поведений она допускает. Это
может привести к появлению ложных контрпримеров, не обнаружи-
ваемых в исходной модели. Выходов из этой ситуации по крайней
