Проблемы параметризованной верификации протоколов когерентности памяти
3
занные с передачей множества сообщений между частями верифици-
руемой системы, к тому же и в некотором необычном порядке, могут
оказаться невыявленными. Формальные методы позволяют получить
математическое доказательство корректности протокола (в пределах
уровня детализации модели), а также могут содействовать получе-
нию тестов, подаваемых на вход RTL-модели верифицируемой мик-
ропроцессорной системы.
В ходе формальной верификации протокола проверяется соответ-
ствие абстрактной модели протокола (
конечного автомата
) его спе-
цификации, т. е. набору свойств, которым должен отвечать протокол.
Формальные методы нацелены на анализ всех достижимых состоя-
ний верифицируемой модели.
Простые методы верификации, основанные на алгоритмах полно-
го перебора пространства глобальных состояний протокола (напри-
мер, анализ достижимости состояний [1–3]), подвержены проблеме
«взрыва числа состояний» и неприменимы для сложных систем даже
с небольшим числом процессорных ядер, не говоря уже о параметри-
зованных системах. «Взрыв числа состояний» – эффект экспоненци-
ального роста числа состояний с ростом числа компонентов, работа-
ющих параллельно.
Существует два класса методов параметризованной верификации
протоколов когерентности:
• основанные на
проверке моделей
(
model checking
) и нацеленные
на максимальную автоматизацию;
• основанные на
доказательстве теорем
(
theorem proving
) и
нацеленные на масштабируемость.
Методы, основанные на model checking.
Model checking [4] —
метод, в ходе применения которого систематически исследуется про-
странство состояний модели верифицируемого протокола с целью
проверки выполнения свойства, описывающего желаемое поведение
протокола. Рассматриваемые модели являются конечными, благодаря
чему задача model checking алгоритмически разрешима, а соответ-
ствующие алгоритмы, как правило, эффективны. Свойства поведения
специфицируются с помощью темпоральной логики, позволяющей
отражать относительный порядок событий без явного указания зна-
чений времени.
К достоинствам model checking относятся:
• полная автоматизация метода;
• генерация контрпримеров, позволяющих отыскать источник
ошибки;
• возможность предоставления частичных спецификаций.
Основным недостатком метода является «взрыв числа состоя-
ний».
