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

h1. Инструкция по установке и настройке Rodin

Для установки Rodin выполните следующие действия:

# Установите Java Runtime Environment (JRE).

# Скачайте архив с Rodin (на данный момент актуальная версия - 3.4): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/

# Распакуйте архив в любом месте на жестком диске и запустите исполняемый файл rodin.

Перед использованием Rodin желательно установить два плагина:

* SMT Solvers Plug-in, инструкция http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in

* Atelier B Provers, набор инструментов автоматического доказательства

Для установки плагина SMT Solvers выполните следующие действия:

# Запустите Rodin и перейдите в раздел Help > Install New Software.

# В выпадающем меню Work with выберите Rodin.

# Появится на выбор несколько категорий с различными плагинами. Разверните категорию Prover Extensions и поставьте галку рядом с SMT Solvers. Нажмите Next.

# Проверьте, что все верно, и нажмите Next.

# Прочитайте и примите условия лицензионного соглашения. Затем нажмите кнопку Finish.

# Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажмите OK.

# Установка может занять некоторое время. По окончанию нажмите на Restart Now.

Установка Atelier B Provers почти не отличается от установки SMT Solvers Plug-in. Отличия:

* На шаге номер 2 в выпадающем меню Work with нужно выбрать Atelier B Provers.

* На шаге номер 3 нужно развернуть категорию Atelier B Provers и поставьте галочку рядом с Atelier B Provers.

После установки плагинов их нужно настроить. Для этого:

# Откройте окно настроек Rodin (пункт Preferences в меню)

# В выпадающем списке меню выберите Event-B -> Sequent Prover -> Auto/Post Tactic

# В выпадающем списке Tactic profile to be used for auto-tactics выберите Default Auto Tactic with SMT

# Уберите галку напротив Enable post-tactic for proving