時間オートマトンによるUMLタイミング図の検証

摘要

従来，UMLは業務系システムのモデリングに適したモデル記述言語として，情報システムの分析·設計·製作·評価の各工程で幅広く用いられてきた．しかし，組込システムの発展により，UMLも，よりハードウエアに近い領域でのソフトウェア設計にも利用できることが求められ，UML2.0よりタイミング図が利用可能となっている．タイミング図はステートマシン図によるオブジェクトの状態遷移と，シーケンス図によるオブジェクト間の相互作用を，時間制約を含む一つのダイアグラムで表現可能であるが，動作のインスタンスごとに記述を行わればならず，システム全体の整合性や正当性を検証することが困難と考えられる．本論文では，複数のタイミング図から，汎用的な単一の時間オートマトンを，関連するオブジェクト毎に作成し，支援ツールUPPAALによりこれらのオートマトンをチャネル接続して，シミュレーションによりもとのタイミング図の整合性·正当性を評価·検証する手法を提案する．