Event-B
リファインメント・モデリングに基づく形式手法
著：中島震
著：來間啓伸
内容紹介
論理的なバクを発生させない形式手法!!Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。 Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。
目次
第1章 形式手法とEvent-B 1.1 形式手法とは 1.2 Event-B 第2章 Event-B 入門 2.1 モデリングの基本的な道具 2.2 リファインメント 2.3 演習問題 第3章 統合ツールRODIN 3.1 RODINツールの概要 3.2 RODINツールの利用 3.3 Event-Bモデルの作成手順 第4章 事例１：図書館システム 4.1 概要 4.2 問題の説明 4.3 考え方 4.4 仕様記述と検証 4.5 演習問題 第5章 事例２：ドアロックシステム 5.1 概要 5.2 問題の説明 5.3 考え方 5.4 仕様記述と検証 5.5 まとめ 第6章 発展的な話題 6.1 振る舞いの検査 6.2 DEPLOYプロジェクト以降のEvent-B 6.2.1 ハイブリッド・システムのモデリングへ 付録 A.1 演習問題の解答例 A.2 Event-B数学記法 A.3 関係と関数
JP-eコード：7649042411000000000J
。出版社：近代科学社
。コンテンツ公開日：2015年02月26日。