Проблемы параметризованной верификации протоколов когерентности памяти
5
мере два: 1) построение точных абстрактных моделей; 2) анализ
контрпримера на ложность и модификация абстрактной модели на
основании полученной информации (
counterexample-guided abstrac-
tion refinement
).
Авторам неизвестно о существовании подхода, применимого к
протоколам когерентности промышленного масштаба, позволяющего
сразу строить точную абстракцию модели протокола. Например, в
литературе отражены абстракция counter abstraction и ее обобщение
environment abstraction [10–12], которые получены путем выделения
набора идентичных процессов в классы эквивалентности на основе
предикатов, которым они удовлетворяют, при этом только один
представитель каждого класса принимается во внимание. Абстракт-
ные модели, полученные с помощью этих методов, являются очень
подробными и, следовательно, будут слишком большими в случае
сложных протоколов. В источниках сообщается о применении этих
абстракций к академическим протоколам. Роль пользователя в этих
методах относительно небольшая. Так, в [11] предлагается подход,
при котором пользователь только описывает протокол на предлагае-
мом входном языке. Далее специальное средство на основе environ-
ment abstraction извлекает из этого описания соответствующую аб-
страктную модель, представляет ее на языке SMV и подает на вход
инструментального средства SMV, проверяющего выполнение
свойств на абстрактной модели.
Существуют методы, нацеленные на нахождение такого числа
K
,
что верификации системы с
K
процессами будет достаточно, чтобы
гарантировать корректность параметризованной системы с
N
процес-
сами для любого
N
. На основании работ в этом и смежном направле-
ниях [13–16] можно сделать вывод, что получаемые значения
K
яв-
ляются слишком большими. Это делает метод неприменимым на
практике. Так, в [14] было найдено
7
K
для протокола когерентно-
сти, основанного на справочнике.
Методы, основанные на доказательстве теорем.
Эффектив-
ность метода model checking ограничена используемыми для проведе-
ния верификации механизмами. Иногда сложность задачи верифика-
ции может быть понижена, если имеется более общее математическое
описание верифицируемого объекта. Такое описание может быть по-
лучено в рамках дедуктивного метода — доказательства теорем.
В ходе доказательства теорем посредством математических рассуж-
дений определяется, удовлетворяет ли спецификации данная реализа-
ция проекта. Реализация и спецификация должны быть представлены в
виде формул некоторой формальной логики. Взаимосвязи между реали-
зацией и спецификацией рассматриваются как теоремы в логике. За-
ключение о соответствии затем выносится путем доказательства теорем.
