試験公開中

このエントリーをはてなブックマークに追加

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

近代科学社

3,800円 1,900円+税 《特価》

UPPAALツール,時間オートマトン,検証したい性質を記述するための時間時相論理に関する知識,および実際の開発で検証の対象となるUML設計仕様のUPPAALによるモデル化方法など,具体的事例も交えてノウハウを解説する.

【注意】本書のEPUB版は固定レイアウト型になっております。文字の大きさの変更や検索、引用などはお使いいただけません。画面の大きい端末でご利用ください。

関連サイト

本書の関連ページが用意されています。

内容紹介

UPPAALは,モデル検査ツールとしては比較的利用が容易ではあるが,実際の開発には多くのハードルがある.本書では,そのようなハードルを乗り越えるために必要な,UPPAALツール,時間オートマトン,検証したい性質を記述するための時間時相論理に関する知識,および実際の開発で検証の対象となるUML設計仕様のUPPAALによるモデル化方法など,具体的事例も交えてノウハウを解説している.

書誌情報

  • 著者: 本位田 真一, 大須賀 昭彦(監修), 長谷川 哲夫, 田原 康之, 磯部 祥尚(著)
  • 発行日: (紙書籍版発行日: 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 年 通商産業省工業技術院電子技術総合研究所
現 在 独立行政法人 産業技術総合研究所主任研究員 工学博士
形式手法による並行システムの検証に関する研究に従事.

目次

第1章 UPPAALを使ってみよう

第2章 UPPAALのシステムモデルと検証式

第3章 検証プロセス

第4章 ケーススタディ(1)オートクラッチ車ギア制御

第5章 ケーススタディ(2)オーディオデータ通信プロトコル

第6章 ソフトウェア設計とモデル検査

第8章 おわりに

付録 演習問題の解答例

Home 書籍一覧 UPPAALによる性能モデル検証:リアルタイムシステムのモデル化とその検証(トップエスイー実践講座5) ▲ ページトップへ戻る