Event-B - 形式手法 Event-BEvent-B † Event-Bは集合論を基礎とした形式手法です。 抽象度の高いモデルをリファインメントすることにより段階的に詳細なモデルを作成します。 詳細なモデルの抽象モデルに対する正当性はリファインメントに関する証明責務を証明することで検証します。 Event-BはB-Methodをベースとしており、多くのコンセプトを共有しています。 開発環境としてEclipseベースのRodin Platformがあります。 Rodin Platformではリファインメント、証明などを支援する機能が提供されています。 また、プラグインにより機能の拡張が可能になっており、多様なプラグインの開発が行われています。 ↑ Documentation † Event-Bの始め方 Event-Bに始めて触れる方向けに学習の流れの一例を掲載しています。 Event-B モデリング言語 証明責務 リファインメン
