B-Methodは、
形式手法に基づいたソフトウェア開発手法であり、その中心となるのはAMN(Abstract Machine Notation)という
仕様記述言語(兼
プログラミング言語)です。B-Methodで使用される
形式手法やツール群は、一般に「B」と呼ばれます。この手法は、
フランスと
イギリスを中心に、Jean-Raymond Abrialによって開発されました。Abrialが開発した
Z言語とも関連性があり、仕様から
プログラミング言語のコード生成をサポートすることを目指しています。
概要
B-Methodは、
ヨーロッパにおいて、
パリのメトロ14号線などの大規模なインフラシステムで実際に利用されています。その堅牢性と商業利用可能なツール群が提供されていることから、産業界からの注目度が高まっています。B-Methodのツール群は、仕様記述、設計、検証、そして最終的なソースコード生成までをカバーしており、ソフトウェア開発の全工程を支援します。
Z言語と比較して、B-Methodは抽象化レベルが低く、単なる
形式仕様記述だけでなく、コードの
詳細化に重点を置いている点が特徴です。そのため、Bで記述された仕様は、
Z言語で記述されたものよりも実装が容易であるとされています。
Event B
Event Bは、B-Methodを拡張したもので、Eclipseと組み合わせて利用することで、対象をより詳細に記述できるようにしたシステムです。Rodin toolやDeployといったプロジェクトによって開発が進められています。Event Bに関する教科書としては、『Modeling in Event-B』が知られており、その表紙には蜂の写真が使われています。
参考文献
B-Methodに関する主要な参考文献として、以下の書籍が挙げられます。
The B-Book: Assigning Programs to Meanings, Jean-Raymond Abrial, Cambridge University Press, 1996年.
The B-Method: An Introduction, Steve Schneider, Palgrave, Cornerstones of Computing series,
2001年.
Software Engineering with B, John Wordsworth, Addison Wesley Longman, 1996年.
The B Language and Method: A Guide to Practical Formal Development, Kevin Lano, Springer-Verlag, FACIT series,
1996年.
Specification in B: An Introduction using the B Toolkit, Kevin Lano, World Scientific Publishing Company, Imperial College Press, 1996年.
Modeling in Event-B, Jean-Raymond Abrial,
2010年
これらの書籍は、B-Methodの基礎から応用までを網羅しており、手法を深く理解する上で非常に役立ちます。
関連項目
B-Methodを理解する上で、以下の関連技術や概念も参考になります。
Z言語
外部リンク
B-Methodに関するより詳しい情報やツールは、以下のリンク先で入手できます。
The B-Method、Virtual Library formal methodsより
Atelier B ツール
B-Core (UK) Ltd
Site B Grenoble
B4free フリーツール
ABTOOLS フリーなB-Methodツール
Rodin event-B オープンソースプラットフォーム
ProB Animator and Model Checker
jbtools B-Method 用パーサおよびエディタ
この記事は、Free On-line Dictionary of Computingから取得した情報を元に、GFDL バージョン1.3以降のライセンス条件に基づいて作成されています。