инструмент Родена

Роден
Оригинальный автор(ы)	Жан-Раймонд Абриаль , Майкл Батлер и др.
Разработчик(и)	Проекты Европейского Союза: РОДЕН (2004–2007) ; РАЗВЕРТЫВАНИЕ (2008–2012 гг.) ; АВАНС (2011–2014 гг.) ;
Первоначальный выпуск	2007
Написано в	Ява
Платформа	Затмение IDE
Тип	Программный инструмент
Лицензия	Открытый исходный код
Веб-сайт	www .event-b .org

Инструмент Rodin — это программный инструмент для формального моделирования в Event-B . ^[1]^[2] Он был разработан в рамках нескольких совместных проектов Европейского Союза , включая проект RODIN (2004–2007 гг.). ^[3]

Обзор

Event-B — это обозначение и метод, разработанные на основе B-метода и предназначенные для использования в поэтапном стиле моделирования . Идея инкрементного моделирования была заимствована из программирования: современные языки программирования имеют интегрированную среду разработки , которая позволяет легко модифицировать и улучшать программы. Инструмент Rodin предоставляет такую среду для Event-B. Двумя характеристиками инструмента Rodin являются простота использования и расширяемость. ^[2]

Инструмент ориентирован на моделирование. Это позволяет пользователю модифицировать модели и опробовать варианты модели. Инструмент также является расширяемым. Это позволяет адаптировать инструмент к конкретным потребностям, поэтому его можно адаптировать к существующим процессам разработки, а не требовать обратного. Существует связанная вики Event-B . ^[4]

Rodin («Строгая открытая среда разработки для сложных систем») — это расширение Eclipse IDE ( на основе Java ). Rodin Eclipse Builder управляет следующим: ^[5]

Проверка правильности формата и типа
Proof obligation (PO) generator
Менеджер по доказательствам (PM)
Распространение изменений

Роден Proof Менеджер (PM)

PM строит дерево доказательств для каждого заказа на покупку.
Автоматический и интерактивный режимы
PM управляет использованными гипотезами
Премьер-министр призывает резонаторов:
- цель разряда, или
- разбить цель на подцели
Сборник рассуждений:
- упрощение, основанное на правилах, процедуры принятия решений,
Базовый язык тактики для определения PM и аргументаторов

Промышленное применение и тематические исследования

Проект Родена включал пять промышленных тематических исследований, которые послужили для проверки набора инструментов и помогли разработать соответствующую методологию их использования. ^[6] Тематические исследования проводились промышленными партнерами проекта Роден при поддержке других партнеров. Тематические исследования были следующими:

Система управления отказами контроллера двигателя;
Часть платформы для мобильных интернет-технологий;
Разработка протоколов связи;
Система отображения воздушного движения;
Приложение для кампуса.

Некоторые доступные плагины для Rodin

B4бесплатные пруверы ^[7]
- Провайдер: ClearSy
- Функция: Доказательства теорем
УМЛ Б ^[8]
- Поставщик: Университет Саутгемптона
- Функция: UML-подобный графический интерфейс для Event-B, поддерживающий диаграммы классов и диаграммы состояний.
Пробник ^[9]^[10]
- Поставщик: Университет Дюссельдорфа
- Функция: Анимация и проверка моделей Event-B; Контрпримеры для целей ложного доказательства, в частности, обязательства по доказательству
Ворота ^[11]
- Провайдер: ClearSy
- Функция: Анимация моделей B. Цель двоякая:
  - Экспериментирование с моделью для наблюдения состояний и переходов.
  - Флэш-анимация моделей Event-B
Модульность ^[12]
- Поставщик: Университет Ньюкасла
- Функция: Структурирование разработок Event-B в логические единицы моделирования, называемые модулями; Модельный состав; Повторное использование модели

Ссылки

^ Абриал, Жан-Раймонд, Майкл Батлер, Стефан Халлерстеде, Тай Сон Хоанг, Фархад Мехта и Лоран Вуазен. (2010). «Роден: открытый набор инструментов для моделирования и рассуждений в Event-B». Международный журнал по программным инструментам для трансфера технологий . 12 : 447–466. дои : 10.1007/s10009-010-0145-y . {{cite journal}}: CS1 maint: несколько имен: список авторов ( ссылка )
^ Перейти обратно: ^а ^б Батлер, Майкл и Стефан Халлерстеде (2007). Инструмент формального моделирования Rodin (PDF) . Рождественский семинар FACS 2007: Формальные методы в промышленности . стр. 1–5. {{cite conference}}: CS1 maint: несколько имен: список авторов ( ссылка )
^ «РОДИН: строгая открытая среда разработки для сложных систем» . Великобритания: Университет Ньюкасла . Проверено 13 июня 2023 г.
^ «Вики-документация Event-B и Родена» . wiki.event-b.org . Проверено 13 июня 2023 г.
^ Батлер, Майкл . «RODIN – инструменты усовершенствования нового поколения» (PDF) . Великобритания: Университет Саутгемптона . Проверено 13 июня 2023 г.
^ «Проект IST-511599 RODIN «Строгая открытая среда разработки сложных систем» » (PDF) . Великобритания: Университет Ньюкасла . Проверено 13 июня 2023 г.
^ «B4free как бесплатный инструмент» . КлирСи . Проверено 13 июня 2023 г.
^ «UML-B: язык моделирования надежных систем» . uml-b.org . Проверено 13 июня 2023 г.
^ «Что такое ПроБ?» . prob.hhu.de . Германия: Университет Дюссельдорфа . Проверено 13 июня 2023 г.
^ Леонова, Мария Александровна и Петр Николаевич Девянин (2022). «Сравнение методов моделирования контроля доступа в ОС и СУБД в Event-B с целью их проверки средствами Rodin и ProB». Прикладная дискретная математика . Приложение 15: 90–99. дои : 10.17223/2226308X/15/22 . {{cite journal}}: CS1 maint: несколько имен: список авторов ( ссылка )
^ «Брама-аниматор для РОДЕНА» . ResearchGate.net . Проверено 13 июня 2023 г.
^ «Плагин модуляризации» . wiki.event-b.org . Проверено 13 июня 2023 г.

Дальнейшее чтение

Жан-Раймон Абриаль . Книга B: Присвоение программам значений . Издательство Кембриджского университета , 1996, ( ISBN 0-521-49619-5 ).
Жан-Раймон Абриаль , Майкл Батлер , Стефан Халлерстед и Лоран Вуазен. Открытая расширяемая инструментальная среда для Event-B. В Z. Liu и J. He , редакторах, ICFEM 2006 , LNCS, том 4260, страницы 588–605. Спрингер, 2006.
Абдолбаги Резазаде, Нил Эванс и Майкл Батлер. Редевелопмент промышленного объекта, практический пример с использованием Event-B и Rodin. На BCS-FACS Рождественской встрече 2007 г. , 2007 г.
РОДЕН. Результат D18: Промежуточный отчет о ходе тематического исследования.
Майкл Батлер и Стефан Халлерстеде, Инструмент формального моделирования Родена , Исследовательский проект ЕС IST 511599 RODIN.
Домашняя страница платформы Eclipse .

Внешние ссылки

[abrial10-1] Абриал, Жан-Раймонд, Майкл Батлер, Стефан Халлерстеде, Тай Сон Хоанг, Фархад Мехта и Лоран Вуазен. (2010). «Роден: открытый набор инструментов для моделирования и рассуждений в Event-B». Международный журнал по программным инструментам для трансфера технологий . 12 : 447–466. дои : 10.1007/s10009-010-0145-y . {{cite journal}}: CS1 maint: несколько имен: список авторов ( ссылка )

[butler07-2] Перейти обратно: ^а ^б Батлер, Майкл и Стефан Халлерстеде (2007). Инструмент формального моделирования Rodin (PDF) . Рождественский семинар FACS 2007: Формальные методы в промышленности . стр. 1–5. {{cite conference}}: CS1 maint: несколько имен: список авторов ( ссылка )

[3] «РОДИН: строгая открытая среда разработки для сложных систем» . Великобритания: Университет Ньюкасла . Проверено 13 июня 2023 г.

[4] «Вики-документация Event-B и Родена» . wiki.event-b.org . Проверено 13 июня 2023 г.

[5] Батлер, Майкл . «RODIN – инструменты усовершенствования нового поколения» (PDF) . Великобритания: Университет Саутгемптона . Проверено 13 июня 2023 г.

[6] «Проект IST-511599 RODIN «Строгая открытая среда разработки сложных систем» » (PDF) . Великобритания: Университет Ньюкасла . Проверено 13 июня 2023 г.

[7] «B4free как бесплатный инструмент» . КлирСи . Проверено 13 июня 2023 г.

[8] «UML-B: язык моделирования надежных систем» . uml-b.org . Проверено 13 июня 2023 г.

[9] «Что такое ПроБ?» . prob.hhu.de . Германия: Университет Дюссельдорфа . Проверено 13 июня 2023 г.

[10] Леонова, Мария Александровна и Петр Николаевич Девянин (2022). «Сравнение методов моделирования контроля доступа в ОС и СУБД в Event-B с целью их проверки средствами Rodin и ProB». Прикладная дискретная математика . Приложение 15: 90–99. дои : 10.17223/2226308X/15/22 . {{cite journal}}: CS1 maint: несколько имен: список авторов ( ссылка )

[11] «Брама-аниматор для РОДЕНА» . ResearchGate.net . Проверено 13 июня 2023 г.

[12] «Плагин модуляризации» . wiki.event-b.org . Проверено 13 июня 2023 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]