ロダンツール

RodinツールはEvent-Bの形式モデリングのためのソフトウェアツールです。^{[ 1 ] [ 2 ]}これは、当初のRODINプロジェクト（2004～2007年）を含む、いくつかの欧州連合の共同プロジェクトの一環として開発されました。^{[ 3 ]}

Event-B は、 B メソッドから発展した表記法と手法であり、増分モデリングスタイルで使用することを目的としています。増分モデリングの考え方はプログラミングから取り入れられたもので、現代のプログラミング言語には、プログラムの変更や改善を容易にする統合開発環境が付属しています。Rodin ツールは、Event-B 用のそのような環境を提供します。Rodin ツールの 2 つの特徴は、使いやすさと拡張性です。^{[ 2 ]}

このツールはモデリングに重点を置いています。ユーザーはモデルを変更したり、モデルのバリエーションを試したりできます。このツールは拡張性も備えています。そのため、特定のニーズに合わせてツールを調整することができ、既存の開発プロセスに適合させることができ、その逆の要求をする必要がありません。関連するEvent-B wikiがあります。^{[ 4 ]}

Rodin（「複雑なシステムのための厳密なオープン開発環境」）は、Eclipse IDE（Javaベース）の拡張機能です。Rodin Eclipse Builderは以下を管理します。^{[ 5 ]}

• 整形式性および型チェッカー
• 債務証明（PO）ジェネレーター
• 校正マネージャー（PM）
• 変更の伝播

ロダン・プルーフ・マネージャー（PM）

• PMは各POに対して証明ツリーを構築する
• 自動モードと対話モード
• PMは使用済みの仮説を管理する
• 首相は理性的な人々にこう呼びかける：
  • 退院目標、または
  • 目標をサブ目標に分割する
• 推論エンジンのコレクション：
  • 簡略化、ルールベース、意思決定手順、
• PMと推論者を定義するための基本的な戦術言語

Rodinプロジェクトには、ツールセットの妥当性を検証し、ツールを使用するための適切な方法論の策定に役立つ5つの産業事例研究が含まれていました。^{[ 6 ]}これらの事例研究は、Rodinプロジェクトの産業パートナーが主導し、他のパートナーが支援しました。事例研究は以下のとおりです。

• エンジン制御装置の故障管理システム。
• モバイルインターネット技術プラットフォームの一部。
• 通信プロトコルの設計。
• 航空交通情報表示システム。
• キャンパス環境に最適なアプリケーション。

• B4free証明者^{[ 7 ]}
  • 提供元：ClearSy
  • 機能: 定理証明器
• UML-B ^{[ 8 ]}
  • 提供元：サウサンプトン大学
  • 機能：クラス図と状態遷移図をサポートする、Event-B用のUMLライクなグラフィカルフロントエンド
• ProB ^{[ 9 ] [ 10 ]}
  • 提供元：デュッセルドルフ大学
  • 機能：イベントBモデルのアニメーションとモデル検査。特に証明義務などの誤った証明目標に対する反例。
• ブラマ^{[ 11 ]}
  • 提供元：ClearSy
  • 機能：Bモデルのアニメーション。目的は2つあります。
    • 状態と遷移を観察するためのモデルを用いた実験
    • Event-Bモデルのフラッシュアニメーション
• モジュール化^{[ 12 ]}
  • 提供元：ニューカッスル大学
  • 機能：Event-Bの開発をモジュールと呼ばれる論理的なモデリング単位に構造化すること。モデルの構成。モデルの再利用。

• ジャン＝レイモン・アブリアル。『Bブック：意味へのプログラムの割り当て』ケンブリッジ大学出版局、1996年、（ISBN） 0-521-49619-5)
• Jean-Raymond Abrial、Michael Butler、Stefan Hallerstede、Laurent Voisin。「Event-B のためのオープンで拡張可能なツール環境」。Z . LiuおよびJ. He編、「ICFEM 2006」、LNCS、第 4260 巻、588～605 ページ。Springer、2006 年。
• Abdolbaghi Rezazadeh、Neil Evans、Michael Butler。「Event-BとRodinを用いた産業施設の再開発に関するケーススタディ」。BCS -FACS Christmas 2007 Meeting、2007年。
• RODIN。成果物D18：ケーススタディの進捗状況に関する中間報告書。
• Michael Butler および Stefan Hallerstede、「Rodin 形式モデリングツール」、EU 研究プロジェクト IST 511599 RODIN。
• Eclipseプラットフォームのホームページ。

• イベントBとロダンプラットフォーム
• Event-BとRodinのドキュメントWiki
• SourceForgeのRodin