Event-B入門

はじめに

Event-Bとは

Event-Bとは、「システムレベルのモデル化と解析のための形式手法」である。Event-Bの特長は以下の３点である。

• 「モデル化表記法での集合論利用」
• 「異なる抽象レベルのシステム表現のためのリファインメントの利用」
• 「リファインメントレベル間の一貫性の検証のための数学的証明の利用」

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. - Event-B.org

Rodin とは

Rodin Platformとは、「リファインメントと数学的証明のための効果的支援を提供するEvent-BのためのEclipseベースのIDE」である。これは「オープンソースであり、Eclipseフレームワークに貢献し、プラグインによってさらなる拡張が可能」である。

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. - Event-B.org