Event-B―リファインメント・モデリングに基づく形式手法 [単行本]

Event-B―リファインメント・モデリングに基づく形式手法 の 商品概要

• 要旨（「BOOK」データベースより）

  そもそも形式手法とは、という話題、Ｅｖｅｎｔ‐Ｂの基本的な考え方、ＲＯＤＩＮツールを用いるＥｖｅｎｔ‐Ｂ仕様作成ならびに検証作業の概要、Ｅｖｅｎｔ‐Ｂの事例として、図書館システム、組込みシステム分野からの事例として、自動車のドアロックシステムを紹介。最後に発展的な話題を簡単にまとめる。

• 目次（「BOOK」データベースより）

  第１章　形式手法とＥｖｅｎｔ‐Ｂ
  第２章　Ｅｖｅｎｔ‐Ｂ入門
  第３章　統合ツールＲＯＤＩＮ
  第４章　事例１：図書館システム
  第５章　事例２：ドアロックシステム
  第６章　発展的な話題

• 著者紹介（「BOOK著者紹介情報」より）（本データはこの書籍が刊行された当時に掲載されていたものです）

  中島 震(ナカジマ シン)
  １９８１年東京大学大学院理学系研究科修士課程修了。現在、国立情報学研究所教授・総合研究大学院大学教授・東京工業大学大学院連携教授。学術博士。この間、科学技術振興機構さきがけ研究員（兼任）、北陸先端科学技術大学院大学客員教授を歴任。形式手法、自動検証、ソフトウェア・モデリングなどの研究に従事
  
  來間 啓伸(クルマ ヒロノブ)
  １９８３年広島大学大学院理学研究科博士課程前期修了。１９８４年株式会社日立製作所。２００６年総合研究大学院大学複合科学研究科修了、博士（学術）。２００７年１０月～２０１４年９月国立情報学研究所特任教授。現在、株式会社日立製作所横浜研究所研究員。形式手法、ソフトウェア工学の研究に従事

• 出版社からのコメント

  Event-Bの入門書。利用するための仕様構築統合環境として、RODINプラットホームを解説。具体的に学べるよう図書館の事例

• 内容紹介

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

• 著者について

  中島 震 (ナカシマ シン)
  中島　震 （国立情報学研究所教授）
  
  來間 啓伸 (クルマ ヒロノブ)
  來間 啓伸（日立製作所）

Event-B―リファインメント・モデリングに基づく形式手法 の商品スペック