トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS

Event-B

Last-modified: 2013-09-23 (月) 16:11:26 (1341d)

Event-B

Event-Bは集合論を基礎とした形式手法です。
抽象度の高いモデルをリファインメントすることにより段階的に詳細なモデルを作成します。
詳細なモデルの抽象モデルに対する正当性はリファインメントに関する証明責務を証明することで検証します。

Event-BはB-Methodをベースとしており、多くのコンセプトを共有しています。

開発環境としてEclipseベースのRodin Platformがあります。
Rodin Platformではリファインメント、証明などを支援する機能が提供されています。
また、プラグインにより機能の拡張が可能になっており、多様なプラグインの開発が行われています。

Documentation

Book

Modeling in Event-B: System and Software Engineering
Jean-Raymond Abrial氏著

書籍に関する情報:
 Event-B.org > Event-B Book
 Event-B and Rodin Documentation Wiki > Event-B Language

 以下のものが公開されています。
  • サンプルチャプター(2章まで)
  • 正誤表
  • 各章のスライド
  • Rodin Platformのアーカイブファイル(ソースコード)
    • 記載されているほぼ全てのものが公開されています。
    • こちらは誤植が修正されているとのことです。

Link