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

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

下記の Wiki に Event-B および Rodin Platform についてまとめています。
＞ http://set.style.coocan.jp/wiki/