AstraVer Toolset » Инструменты дедуктивной верификации моделей политик безопасности

h1. Сборка модели и воспроизведение доказательств

Для подтверждения того, что модель полностью доказана, ее необходимо собрать (build). В ходе сборки Rodin сначала сгенерирует утверждения для доказательства (proof obligations), а потом попробует применить к ним сохраненные в модели доказательства.

Для сборки модели необходимо в левой части интерфейса Rodin в окне Event-B Explorer щелкнуть правой кнопкой мыши по названию модели и выбрать в выпадающем меню Build Project:

!build-project.png!

После завершения сборки необходимо убедиться, что сгенерированные утверждения для доказательства каждого компонента модели (каждой машины и контекста) были успешно доказаны (помечены зелеными галочками):

!pos.png!

Если это так, то модель является полностью доказанной.