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

• 資料種別: 図書
• ISBN: 978-4-7649-0424-8
• タイトル: Event-B : リファインメント・モデリングに基づく形式手法
• タイトルよみ: イヴェントビー : リファインメント モデリング ニ モトズク ケイシキ シュホウ
• 著者・編者: 中島震, 來間啓伸 共著
• 著者標目: 中島, 震, 1955- ナカジマ, シン, 1955- ( 00892083 )典拠; 来間, 啓伸 クルマ, ヒロノブ ( 01115484 )典拠
• 出版事項: 東京 : 近代科学社
• 出版年月日等: 2015.2
• 出版年（W3CDTF）: 2015
• 数量: 161p
• 大きさ: 24cm
• 出版地（国名コード）: JP
• 本文の言語コード: jpn
• 件名標目: ソフトウェア工学 ソフトウェアコウガク ( 01014113 )典拠
• NDC9版: 007.61 : 情報科学
• NDLC: M159
• 対象利用者: 一般
• 書誌注記: 文献あり 索引あり
• 入手条件・定価: 3800円
• 所蔵機関: 国立国会図書館
• 請求記号: M159-L622
• 連携機関・データベース: 国立国会図書館 : 国立国会図書館蔵書; https://ndlsearch.ndl.go.jp
• 書誌ID（NDLBibID）: 026100868; http://id.ndl.go.jp/bib/026100868
• 全国書誌番号: 22539717
• トーハンMARC番号: 33224012
• 目録規則: 日本目録規則1987年版改訂版
• 整理区分コード: 111

• 要約等: Event-Bの入門書。利用するための仕様構築統合環境として、RODINプラットホームを解説。具体的に学べるよう図書館の事例（提供元: 出版情報登録センター（JPRO））
• 著者紹介: 中島 震 中島 震 （国立情報学研究所教授）來間 啓伸 來間 啓伸（日立製作所）（提供元: 出版情報登録センター（JPRO））

目次

第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 関係と関数