Event-B - リファインメント・モデリングに基づく形式手法

著者名：中島震/來間啓伸

近代科学社（2018/08発売）

• ISBN：9784764904248

内容説明

論理的なバグを発生させない形式手法!!　Event-Bはパリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄などの無人運転を成功に導いたJ.R.アブリエル氏が考案した新しい形式仕様言語である。本書では入門書として実際に利用するための仕様構築統合環境のRODINプラットホームを使って解説する。具体的な事例として図書館、自動車のドアロック・システムを紹介している。

目次

1. 形式手法とEvent-B
2. Event-B入門
3. 統合ツールRODIN
4. 事例1：図書館システム
5. 事例2：ドアロックシステム
6. 発展的な話題

感想・レビュー

※以下の感想・レビューは、株式会社ドワンゴの提供する「読書メーター」によるものです。

[TUI]

Event-Bの理論的背景のエッセンスを解説したって感じかな。一応、Event-B用IDE(って言っていいのかな？)であるRodinにも触れてるけど、かなり大雑把な説明だけ。事例の章がRodinを使ったハンズオン的なものだとよかったんだけど。

2015/09/15