верификаторе отличается от стандартной схемы, используемой,
например, верификатором Converter.
Входной язык верификатора Bogor, который называется BIR, может
быть расширен новыми, сложными типами данных, которые
представляют собой классы, имеющие внутренние состояния.
У класса можно вызывать действия, которые могут изменить
внутреннее состояние, или запрашивать значения тех или иных
внутренних переменных. При определенных ограничениях на новый
класс средство Bogor может верифицировать модели, которые
используют объекты нового класса.
Возможность расширить входной язык позволяет абстрагироваться от
лишних деталей описания верифицируемой модели, что теоретически
приводит к меньшему числу элементарных состояний модели, а
следовательно, и к более простой и быстрой верификации.
В верификаторе UniMod.Verifier был реализован новый класс,
содержащий в себе описание автоматной системы в целом. Этот класс
выполняет лишь одно действие «step»: обработать очередное событие.
При вызове этого действия класс недетерминированно выбирает
событие и отдает его на обработку автоматной программе. Благодаря
использованию нового класса, описание модели на входном языке
верификатора Bogor свелось к тривиальному бесконечному циклу из
одного состояния. В этом состоянии у объекта нового класса
вызывается действие step.
Основное достоинство такого подхода состоит в том, что описание
программы на входном языке верификатора стало тривиальным и
одинаковым для любой автоматной программы. Логика работы
модели и хранение состояний автоматов реализуется программно и
один раз для всех автоматных систем. Нет необходимости
генерировать новые промежуточные входные данные для каждой
верифицируемой автоматной программы.
Кроме того, в верификаторе UniMod.Verifier применяется еще одно
оригинальное решение. В других верификаторах (например, в
Converter) используется разная реализация автоматов в рабочей
программе и при верификации. В верификаторе Converter автоматная
программа запускается и работает при помощи интерпретатора
инструментального средства UniMod. Однако при верификации
проверяется корректность автоматной программы, реализованной на
языке Promela. При этом нет гарантий, что логика работы автоматной
программы реализована одинаково в интерпретаторе
инструментального средства UniMod и на языке Promela. В случае же
использования UniMod.Verifier можно сказать, что программа Bogor