Event-B リファインメント・モデリングに基づく形式手法（近代科学社） [電子書籍]

Event-B リファインメント・モデリングに基づく形式手法（近代科学社） の 商品概要

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

• 目次

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

• 商品の注意点

  この商品は固定レイアウトで作成されており、タブレットなど大きいディスプレイを備えた端末で読むことに適しています。購入前にお使いの端末で無料サンプルをお試しください。
  

Event-B リファインメント・モデリングに基づく形式手法（近代科学社） の商品スペック