摘要 : 分散実時間アプリケーションにおいては．ユーザに対して提供されるQoS（Quality of Service）を保証することがきわめて重要である．特に，時間qoSに対する要求の保証が重要視ざれている．本稿では，UML/OCLに記述された時間QoSを多段階かつ階層的に... 展开 分散実時間アプリケーションにおいては．ユーザに対して提供されるQoS（Quality of Service）を保証することがきわめて重要である．特に，時間qoSに対する要求の保証が重要視ざれている．本稿では，UML/OCLに記述された時間QoSを多段階かつ階層的に検証する方法を提案する．コンポーネントの時間的振る舞し、を時間オートマントで抽象化した抽象QoSモデルを利用することで，時間QoSを多段牌かつ階層的に形式的に保証する.これにより，状態爆発など既存の手法が抱える問題を解消し，効率的に時間Qosの整合性の判定が可能となる．提案手法をUPPAALを用いて例題に適用した結鼠　 検証時間の観点から見て有用であることがわかった． 收起