Event-B：リファインメント・モデリングに基づく形式手法
中島 震
近代科学社本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。
【注意】本書のEPUB版は固定レイアウト型になっております。文字の大きさの変更や検索、引用などはお使いいただけません。画面の大きい端末でご利用ください。
書籍情報
著者: 中島 震
共著者: , 來間 啓伸
発行日: 2016-04-28
最終更新日: 2016-04-28
バージョン: 1.0.0
ページ数: 176ページ(PDF版換算)ページ
対応フォーマット: PDF, EPUB
出版社: 近代科学社
対象読者
形式手法, モデリング, 形式仕様, 仕様記述に興味のある方
著者について
1981 年 東京大学大学院理学系研究科修士課程 修了
現 在 国立情報学研究所 教授・総合研究大学院大学 教授・東京工業大学大学院 連携教授 学術博士
この間，科学技術振興機構さきがけ研究員（兼任），北陸先端科学技術大学院大学 客員教授を歴任．
形式手法，自動検証，ソフトウェア・モデリングなどの研究に従事．
目次
第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 関係と関数