0pt

UPPAALによる性能モデル検証―リアルタイムシステムのモデル化とその検証 (トップエスイー実践講座)

長谷川 哲夫, 磯部 祥尚, 田原 康之 | 近代科学社 | 2012-09-01

実時間システム開発向けモデル検査ツールの標準UPPAALの日本初の解説書。組込みシステムの仕様や設計のモデリングと、機能や性能に関するモデル検査、開発プロセスの設計のための実用書。 第1章 UPPAALを使ってみよう 第2章 UPPAALのシステムモデルと検証式 第3章 検証…

0pt

0pt

VDM++による形式仕様記述 (トップエスイーシリーズ 実践講座)

石川 冬樹 | 近代科学社 | 2011-07-27

実用システム開発ではまず仕様を書こう!明確な仕様の記述と検証を行わずして正統な開発を行うことはできない-何を開発するのかを表す仕様の実践的なモデリングと、仕様書を基盤とする開発者間の建設的な対話に向けて。 形式手法とVDM VDM概要 VDM++記述の構成要素 VDM++によ…

0pt

0pt

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

中島 震, 來間 啓伸 | 近代科学社 | 2015-02-26

Event-Bの入門書。利用するための仕様構築統合環境として、RODINプラットホームを解説。具体的に学べるよう図書館の事例 論理的なバクを発生させない形式手法!! Event-Bは、パリ地下鉄、ニューヨーク地下鉄、バルセロナ地下鉄、ドゴール空港のシャトルの無人運転を成功に導…

0pt

0pt

形式手法入門―ロジックによるソフトウェア設計―

中島 震 | オーム社 | 2012-04-20

1章 論理で考える 2章 指先で考える 3章 機能仕様を論理で考える 4章 リファインメントを検査する 5章 オブジェクト指向デザインを検査する 6章 振る舞い仕様を検査する 7章 プログラム検査を論理で考える 付録 モデル規範形式手法の流れ

0pt