仕様の段階で誤りをなくす注目の手法「Bメソッド」を実践活用するための解説書。安心安全を含めてますます高度な機能や性能が要求されるソフトウェアシステムの開発において、厳密な仕様記述を基に開発を行う形式手法に対する関心と期待が高まっている。本書は、我が国初のBメソッドの書き下ろし入門書である。実際の開発への適用を意識した実用指向の内容が、平明でわかりやすく記述されている。

論理的なバクを発生させない形式手法!!
Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。
Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。
本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。
形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。