UPPAALによる性能モデル検証 ― リアルタイムシステムのモデル化とその検証

本位田真一大須賀昭彦長谷川哲夫田原康之磯部祥尚

近代科学社

発売：2018/08/01

発行形態：書籍

ファイル：PDF形式／7.2MB

ポイント：38pt

¥4,180( 本体 ¥3,800 )

商品詳細

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

第1章　UPPAALを使ってみよう
第2章　UPPAALのシステムモデルと検証式
第3章　検証プロセス
第4章　ケーススタディ(1)オートクラッチ車ギア制御
第5章　ケーススタディ(2)オーディオデータ通信プロトコル
第6章　ソフトウェア設計とモデル検査
第8章　おわりに

付録　演習問題の解答例

購入前の注意点

・3Dセキュア導入とクレジットカードによるお支払いについて
・この書籍はKinoppy for iOS、Kinoppy for Android、Kinoppy for Windows または Kinoppy for Mac（いずれも最新版）でお読みください。
・電子書籍は会員サービス利用規約に則してご利用いただきます。
・海外会員様にはプレゼントを贈れません。

著者情報

大須賀昭彦［オオスガアキヒコ］
１９８１年上智大学理工学部数学科卒業。株式会社東芝。１９８５年～１９８９年（財）新世代コンピュータ技術開発機構（ＩＣＯＴ）。１９９５年工学博士（早稲田大学）。現在、電気通信大学大学院情報システム学研究科教授。ＩＥＥＥ　Ｃｏｍｐｕｔｅｒ　Ｓｏｃｉｅｔｙ　Ｊａｐａｎ　Ｃｈａｐｔｅｒ　Ｃｈａｉｒ、人工知能学会理事、日本ソフトウェア科学会理事などを歴任。ソフトウェア工学、人工知能の研究に従事

長谷川哲夫［ハセガワテツオ］
１９８７年早稲田大学大学院理工学研究科電気工学修士課程修了。現在、株式会社東芝ソフトウエア技術センター。ソフトウェア工学、自律分散システム、仮想化技術などの研究開発に従事

田原康之［タハラヤスユキ］
１９９１年東京大学大学院理学系研究科修士課程修了。株式会社東芝。２００３年国立情報学研究所。現在、電気通信大学大学院情報システム学研究科准教授、博士（情報科学）。エージェント技術、ソフトウェア工学の研究に従事。特に、エージェント指向開発方法論、モデル検査技術、および要求分析技術に興味を持つ

磯部祥尚［イソベヨシナオ］
１９９２年芝浦工業大学大学院電気工学専攻修士課程修了。通商産業省工業技術院電子技術総合研究所。現在、独立行政法人産業技術総合研究所主任研究員、工学博士。形式手法による並行システムの検証に関する研究に従事（本データはこの書籍が刊行された当時に掲載されていたものです）

このシリーズの商品

n

  • Bメソッドによる形式仕様記述 ― ソフトウェアシステムのモデル化とその検証

  • ソフトウェアパターン ― パターン指向の実践ソフトウェア開発

  • SPINによる設計モデル検証 ― モデル検査の実践ソフトウェア検証

  • VDM++による形式仕様記述 ― 形式仕様入門・活用の第一歩

  • UPPAALによる性能モデル検証 ― リアルタイムシステムのモデル化とその検証

  • 並行システムの検証と実装 ― 形式手法CSPに基づく高信頼並行システム開発入門

まとめ買い

この著者の他の商品・シリーズ

n

  • 考えるコンテンツ「スマーティブ」

  • Bメソッドによる形式仕様記述 ― ソフトウェアシステムのモデル化とその検証

  • ソフトウェアパターン ― パターン指向の実践ソフトウェア開発

  • ソフトウェア科学基礎 ― 最先端のソフトウェア開発に求められる数理的基礎

  • 実践的ソフトウェア工学 ― 実践現場から学ぶソフトウェア開発の勘所

  • 要求工学概論 ― 要求工学の基本概念から応用まで

  • VDM++による形式仕様記述 ― 形式仕様入門・活用の第一歩

  • 並行システムの検証と実装 ― 形式手法CSPに基づく高信頼並行システム開発入門

  • SPINによる設計モデル検証 ― モデル検査の実践ソフトウェア検証

  • IT Text 人工知能（改訂2版）