В.С. Буренков, С.Р. Иванов
6
Средство автоматизированного доказательства теорем (theorem
prover) — это программный инструмент, определяющий истинность
формул в заданной логике. Популярными инструментами являются
ACL2, Coq, HOL, Isabelle, NuPrl, PVS. Логики, на которых основаны
эти средства, очень разнообразны, но общим аспектом является их
выразительность. Однако выразительность логики влечет за собой ее
неразрешимость, что означает невозможность построения такой ав-
томатической процедуры (или алгоритма), которая, приняв на вход
формулу, всегда может определить вывод этой формулы в данной
логике. Использование средств автоматизированного доказательства
теорем подразумевает взаимодействие с пользователем-экспертом и
является сложным творческим процессом. Помимо этого, если дока-
зательство теоремы завершается неудачей, очень сложно на основе
этой информации найти ошибку в верифицируемой системе. Пре-
имуществом дедуктивной верификации является возможность рабо-
ты с системами с бесконечным числом состояний. В дальнейшем под
доказательством теорем будем понимать любой метод, требующий от
пользователя вспомогательных утверждений о верифицируемой си-
стеме.
В [17] Парк применил средство автоматизированного доказатель-
ства теорем общего назначения PVS [18] для параметризованной ве-
рификации протокола когерентности FLASH [19]. Данный процесс
очень сложен, так как требует от пользователя индуктивных инвари-
антов. Маловероятно, что методы, основанные только на доказатель-
стве теорем, могут найти применение при верификации протоколов
современных мультипроцессоров.
В [20] изложен метод параметризованной верификации протоко-
лов когерентности памяти, основанный на композиционной проверке
моделей и реализованный в системе Cadence SMV. Задав свойство
относительно некоторого кэша системы, изначально делают попытку
проверить это свойство на грубой абстрактной модели, в которой от-
ражен соответствующий процесс, а все остальные процессы замене-
ны абстрактным процессом. Вероятной причиной полученного
контрпримера является сообщение от абстрактного процесса. Чтобы
избавиться от контрпримера, предлагается две стратегии: добавить
отправителя сообщения в абстракцию в виде отдельного процесса
(что не может быть осуществлено много раз, так как ведет к «взрыву
числа состояний») или ввести лемму, исключающую некорректную
отправку сообщения. Процесс повторяется до тех пор, пока не будут
исключены все ложные контрпримеры и проверены все свойства
спецификации.
Преимущество метода заключается в следующем: отсутствует
необходимость предоставлять индуктивные инварианты, поскольку
