試験公開中

このエントリーをはてなブックマークに追加

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

近代科学社

3,800円+税

本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。

【注意】本書のEPUB版は固定レイアウト型になっております。文字の大きさの変更や検索、引用などはお使いいただけません。画面の大きい端末でご利用ください。

関連サイト

本書の関連ページが用意されています。

内容紹介

論理的なバクを発生させない形式手法!!

Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。

書誌情報

  • 著者: 中島 震, 來間 啓伸
  • 発行日: (紙書籍版発行日: 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章 事例1:図書館システム

  • 4.1 概要
  • 4.2 問題の説明
  • 4.3 考え方
  • 4.4 仕様記述と検証
  • 4.5 演習問題

第5章 事例2:ドアロックシステム

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

参考文献

索 引

Home 書籍一覧 Event-B:リファインメント・モデリングに基づく形式手法 ▲ ページトップへ戻る