On the implementation of a formal method for verification of scalable cache coherent systems

В работе приведен анализ существующих методов верификации протоколов когерентности кэш-памяти масштабируемых систем. Рассмотрены методы проверки моделей и дедуктивной верификации, методы композиционной верификации и методы, основанные на абстракциях. На основании литературы изложен формальный метод параметризованной проверки свойств безопасности протоколов когерентности. Предложенный метод основан на синтаксических преобразованиях Promela-моделей. Рассмотрена математическая модель протоколов когерентности кэш-памяти в виде системы переходов. Представлена абстрактная модель протоколов наряду с трансформациями исходной модели, которые позволяют ее получить. Размер абстрактной модели не зависит от количества процессорных узлов верифицируемой системы. Предложена архитектура системы верификации протоколов когерентности. Данная система имеет целью объединить различные этапы процесса верификации воедино и автоматизировать выполнение трудоемких задач, решение которых легко получить алгоритмически, а попытки сделать это вручную чреваты внесением в модель ошибок. Основной частью архитектуры является транслятор языка Promela во внутреннее представление и подсистема анализа и модификации внутреннего представления. Описано применение метода к верификации протокола German, построение и анализ соответствующей Promela-модели. Приведены примеры абстрактных преобразований. Проанализированы результаты проверки двух ошибочных версий протокола German, представленных в литературе. Указаны недостатки рассмотренного метода. Например, использование ограниченного подмножества языка Promela создает разработчикам моделей дополнительные трудности и приводит к неестественным моделям. Сформулированы направления по улучшению, в частности, расширению набора поддерживаемых конструкций языка Promela, и автоматизации метода, необходимые для проведения верификации многоядерных