情報
Event-Bリファインメント・モデリングに基づく形式手法
論理的なバクを発生させない形式手法!!
Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。
Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。
本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。
形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。
電子書籍¥4,180 小売希望価格（税込）
紙の書籍¥4,180定価（税込）
基本情報
| 発売日 | 2015年2月26日 |
|---|---|
| 本体価格 | 3,800円 |
| ページ数 | 176 ページ ※印刷物 |
| サイズ | B5 変形 |
| ISBN | 9784764904248 |
| ジャンル | 情報 |
| タグ | 要求仕様 |
| 電子書籍形式 | 固定型 |
主要目次
第 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
付録
A.1 演習問題の解答例
A.2 Event-B 数学記法
A.3 関係と関数
目 次
参考文献
索 引
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
付録
A.1 演習問題の解答例
A.2 Event-B 数学記法
A.3 関係と関数
目 次
参考文献
索 引