Инструмент Rodin - это инструмент для формального моделирования в Event-B. Событие-B - это обозначение и метод, разработанный на основе B-метода, который предназначен для использования с поэтапным стилем моделирования . Идея инкрементального моделирования взята из программирования: современные языки программирования имеют интегрированную среду разработки.которые позволяют легко изменять и улучшать программы. Инструмент Rodin предоставляет такую среду для Event-B. Две основные характеристики инструмента Rodin - это простота использования и расширяемость. Инструмент ориентирован на моделирование. Модифицировать модели и опробовать варианты модели легко. Инструмент также можно легко расширить. Это позволяет адаптировать инструмент к конкретным потребностям, так что инструмент может быть адаптирован для соответствия существующим процессам разработки, вместо того, чтобы требовать обратного. Вики -сайт Event-B - полезный ресурс для пользователей и разработчиков.
Rodin (строгая открытая среда разработки для сложных систем) - это расширение Eclipse IDE (на основе Java). Координаты Rodin Eclipse Builder:
- Правильный формат + проверка шрифтов
- Генератор доказательств (PO)
- Proof manager (PM)
- Распространение изменений
Роден Пруф Менеджер (PM)
- PM строит дерево доказательств для каждого PO
- Автоматический и интерактивный режимы
- PM управляет использованными гипотезами
- PM призывает рассуждающих к
- цель разряда, или
- разделить цель на подцели
- Сборник рассуждений:
- упрощение, основанное на правилах, процедуры принятия решений,…
- Базовый язык тактик для определения PM и рассуждающих
Промышленные приложения и тематические исследования
Проект Rodin включал пять промышленных тематических исследований, которые служили для проверки набора инструментов и помогли разработать соответствующую методологию использования инструментов. Кейс-стади проводились промышленными партнерами проекта «Родин» при поддержке других партнеров. Тематические исследования были следующими:
- система управления отказами для контроллера двигателя
- часть платформы для мобильных интернет-технологий
- разработка протоколов связи
- система отображения воздушного движения
- приложение для окружающего кампуса
Некоторые доступные плагины для Родина
- B4free пруверы
- Провайдер: ClearSy
- Функция: средства доказательства теорем
- UML-B
- Провайдер: Саутгемптонский университет
- Функция: UML-подобный графический интерфейс для Event-B, поддерживающий диаграммы классов и диаграммы состояний
- ProB
- Провайдер: Дюссельдорфский университет
- Функции: Анимация и модельная проверка моделей Event-B; Контрпримеры для ложных целей доказательства, в частности, обязательств по доказыванию
- Брама
- Провайдер: ClearSy
- Функция: Анимация моделей B. Цель двоякая:
- экспериментирование с моделью для наблюдения состояний и переходов
- Флэш-анимация моделей Event-B
- Модуляризация
- Провайдер: Университет Ньюкасла
- Функция: структурирование событий Event-B в логические единицы моделирования, называемые модулями; Модельный состав; Повторное использование модели
Рекомендации
- Жан-Раймон Абриаль . Книга B: Присвоение программ смыслам. Издательство Кембриджского университета, 1996, ( ISBN 0-521-49619-5 ).
- Жан-Раймон Абриаль , Майкл Батлер, Стефан Халлерстеде и Лоран Вуазен. Открытая расширяемая инструментальная среда для Event-B. В З. Лю и Дж. Хэ, редакторы, ICFEM 2006, том 4260, страницы 588–605. Спрингер, 2006.
- Абдолбаги Резазаде, Нил Эванс и Майкл Батлер. Редевелопмент индустриального, кейс с использованием Event-B и Rodin. В BCS-FACS Christmas 2007 Meeting, 2007.
- РОДИН. Результат D18: Промежуточный отчет о развитии тематических исследований.
- Майкл Батлер и Стефан Халлерстеде: Инструмент формального моделирования Родена, исследовательский проект ЕС IST 511599 RODIN
- Затмение . Домашняя страница платформы Eclipse.
Эта статья основана на материалах, взятых из Free On-line Dictionary of Computing до 1 ноября 2008 г. и включенных в соответствии с условиями «перелицензирования» GFDL версии 1.3 или новее.