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

• Material Type: 図書
• ISBN: 978-4-7649-0424-8
• Title: Event-B : リファインメント・モデリングに基づく形式手法
• Title Transcription: イヴェントビー : リファインメント モデリング ニ モトズク ケイシキ シュホウ
• Author/Editor: 中島震, 來間啓伸 共著
• Author Heading: 中島, 震, 1955- ナカジマ, シン, 1955- ( 00892083 )Authorities; 来間, 啓伸 クルマ, ヒロノブ ( 01115484 )Authorities
• Publication, Distribution, etc.: 東京 : 近代科学社
• Publication Date: 2015.2
• Publication Date (W3CDTF): 2015
• Extent: 161p
• Size: 24cm
• Place of Publication (Country Code): JP
• Text Language Code: jpn
• Subject Heading: ソフトウェア工学 ソフトウェアコウガク ( 01014113 )Authorities
• NDC 9th ed.: 007.61 : Information science
• NDLC: M159
• Target Audience: 一般
• Note (Bibliography): 文献あり 索引あり
• Price: 3800円
• Holding library: 国立国会図書館
• Call No.: M159-L622
• Data Provider (Database): 国立国会図書館 : 国立国会図書館蔵書; https://ndlsearch.ndl.go.jp
• Bibliographic ID (NDL): 026100868; http://id.ndl.go.jp/bib/026100868
• National Bibliography No. (JPNO): 22539717
• TOHAN MARC No.: 33224012
• Cataloging Rule: Nippon Cataloguing Rules 1987 Revised Edition
• Bibliographic Record Category (NDL): 111

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

Table of Contents

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