内容説明
UPPAALは,モデル検査ツールとしては比較的利用が容易ではあるが,実際の開発には多くのハードルがある.本書では,そのようなハードルを乗り越えるために必要な,UPPAALツール,時間オートマトン,検証したい性質を記述するための時間時相論理に関する知識,および実際の開発で検証の対象となるUML設計仕様のUPPAALによるモデル化方法など,具体的事例も交えてノウハウを解説している.
目次
第1章 UPPAALを使ってみよう
第2章 UPPAALのシステムモデルと検証式
第3章 検証プロセス
第4章 ケーススタディ(1)オートクラッチ車ギア制御
第5章 ケーススタディ(2)オーディオデータ通信プロトコル
第6章 ソフトウェア設計とモデル検査
第8章 おわりに
付録 演習問題の解答例
感想・レビュー
※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。
kaizen@名古屋de朝活読書会
31
#感想 #短歌 uppaalの反例追跡容易かな現象挙動原因分析 #説明歌 uppaalは図入力が簡単で時間と状態遷移設計 2016/01/30
Q
1
某RTOSがTLA+とUPPAALでモデル検査されていると聞いて読みました。残念ながらツール自体が商用利用有料だったので、雰囲気だけ掴む程度に。時間制約をGUIを使ったオートマトンで記述し、シミュレーションもしくは検証するようです。またステートチャートとオートマトンの比較も参考になりました。しかし事例を読む限りでは小さな対象でも大きな図になってしまうように思えて自分で使える実感は得られませんでした。それでもこのツールの理論的な基礎であるTCTLに興味がわきました。2019/01/18