関連サイト
本書の関連ページが用意されています。
内容紹介
論理的なバクを発生させない形式手法!!
Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。
書誌情報
- 著者: 中島 震, 來間 啓伸
- 発行日: 2016-04-28 (紙書籍版発行日: 2015-02-26)
- 最終更新日: 2016-04-28
- バージョン: 1.0.0
- ページ数: 176ページ(PDF版換算)
- 対応フォーマット: PDF, EPUB
- 出版社: 近代科学社
対象読者
形式手法, モデリング, 形式仕様, 仕様記述に興味のある方
著者について
中島 震
1981 年 東京大学大学院理学系研究科修士課程 修了
現 在 国立情報学研究所 教授・総合研究大学院大学 教授・東京工業大学大学院 連携教授 学術博士
この間，科学技術振興機構さきがけ研究員（兼任），北陸先端科学技術大学院大学 客員教授を歴任．
形式手法，自動検証，ソフトウェア・モデリングなどの研究に従事．
來間 啓伸
1983 年 広島大学大学院理学研究科博士課程前期 修了
1984 年 株式会社日立製作所
2006 年 総合研究大学院大学複合科学研究科 修了 博士（学術）
2007 年10 月～ 2014 年9 月 国立情報学研究所 特任教授
現 在 株式会社日立製作所 横浜研究所 研究員
形式手法，ソフトウェア工学の研究に従事．
目次
第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 関係と関数