出版社内容情報
論理的なバクを発生させない形式手法!!
Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導いた、J.R.アブリエル氏が考案した新しい形式仕様言語である。
Event-Bは、仕様記述の単位をイベントとし、基礎となる集合論などはBメソッドの考え方を継承する。
本書は、Event-Bの入門書である。また実際に利用するための仕様構築統合環境として、RODINプラットホームの利用方法を解説する。具体的に学べるよう図書館の事例や、組込みとして自動車のドアロック・システムを紹介している。
形式手法や、形式仕様言語を学ぶ技術者や研究者には最適の書である。
内容説明
そもそも形式手法とは、という話題、Ｅｖｅｎｔ‐Ｂの基本的な考え方、ＲＯＤＩＮツールを用いるＥｖｅｎｔ‐Ｂ仕様作成ならびに検証作業の概要、Ｅｖｅｎｔ‐Ｂの事例として、図書館システム、組込みシステム分野からの事例として、自動車のドアロックシステムを紹介。最後に発展的な話題を簡単にまとめる。
目次
第１章 形式手法とＥｖｅｎｔ‐Ｂ
第２章 Ｅｖｅｎｔ‐Ｂ入門
第３章 統合ツールＲＯＤＩＮ
第４章 事例１：図書館システム
第５章 事例２：ドアロックシステム
第６章 発展的な話題
著者等紹介
中島震［ナカジマシン］
１９８１年東京大学大学院理学系研究科修士課程修了。現在、国立情報学研究所教授・総合研究大学院大学教授・東京工業大学大学院連携教授。学術博士。この間、科学技術振興機構さきがけ研究員（兼任）、北陸先端科学技術大学院大学客員教授を歴任。形式手法、自動検証、ソフトウェア・モデリングなどの研究に従事
來間啓伸［クルマヒロノブ］
１９８３年広島大学大学院理学研究科博士課程前期修了。１９８４年株式会社日立製作所。２００６年総合研究大学院大学複合科学研究科修了、博士（学術）。２００７年１０月～２０１４年９月国立情報学研究所特任教授。現在、株式会社日立製作所横浜研究所研究員。形式手法、ソフトウェア工学の研究に従事（本データはこの書籍が刊行された当時に掲載されていたものです）
※書籍に掲載されている著者及び編者、訳者、監修者、イラストレーターなどの紹介情報です。
感想・レビュー
※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。
TUI
