関連サイト
本書の関連ページが用意されています。
内容紹介
UPPAALは，モデル検査ツールとしては比較的利用が容易ではあるが，実際の開発には多くのハードルがある．本書では，そのようなハードルを乗り越えるために必要な，UPPAALツール，時間オートマトン，検証したい性質を記述するための時間時相論理に関する知識，および実際の開発で検証の対象となるUML設計仕様のUPPAALによるモデル化方法など，具体的事例も交えてノウハウを解説している．
書誌情報
- 著者: 本位田 真一, 大須賀 昭彦(監修), 長谷川 哲夫, 田原 康之, 磯部 祥尚(著)
- 発行日: 2018-03-23 (紙書籍版発行日: 2012-09-30)
- 最終更新日: 2018-03-23
- バージョン: 1.0.0
- ページ数: 207ページ(PDF版換算)
- 対応フォーマット: PDF, EPUB
- 出版社: 近代科学社
対象読者
UPPAAL,ソフトウェア設計,モデル検査に興味がある人
著者について
本位田 真一
1978年 早稲田大学大学院理工学研究科博士前期課程 修了
1978年 株式会社 東芝
現 在 国立情報学研究所 教授・東京大学大学院情報理工学系研究科 教授 工学博士
大須賀 昭彦
1981 年 上智大学理工学部数学科 卒業
1981 年 株式会社 東芝
1985 年〜1989 年 （財）新世代コンピュータ技術開発機構（ICOT）
1995 年 工学博士（早稲田大学）
現 在 電気通信大学大学院情報システム学研究科 教授
IEEE Computer Society Japan Chapter Chair，人工知能学会理事，日本ソフトウェア科学会理事などを歴任．ソフトウェア工学，人工知能の研究に従事．
長谷川 哲夫
1987 年 早稲田大学大学院理工学研究科電気工学修士課程 修了
現 在 株式会社 東芝 ソフトウエア技術センター
ソフトウェア工学，自律分散システム，仮想化技術などの研究開発に従事．
田原 康之
1991 年 東京大学大学院理学系研究科修士課程 修了
1991 年 株式会社 東芝
2003 年 国立情報学研究所
現 在 電気通信大学大学院情報システム学研究科 准教授 博士（情報科学）
エージェント技術，ソフトウェア工学の研究に従事．特に，エージェント指向開発方法論，モデル検査技術，および要求分析技術に興味を持つ．
磯部 祥尚
1992 年 芝浦工業大学大学院電気工学専攻修士課程 修了
1992 年 通商産業省工業技術院電子技術総合研究所
現 在 独立行政法人 産業技術総合研究所主任研究員 工学博士
形式手法による並行システムの検証に関する研究に従事．