UML/OCLに記述された時間 QoS の階層的検証手法の提案

長井, 栄吾; 岡野, 浩三; 楠本, 真二

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2006, 106(202), 13-18

アクセス数:215件（2025-05-11 23:27 集計）

固定URL: https://hdl.handle.net/11094/27421

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
itr106_202_013 pdf なし 628 KB 59 2014.04.11  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
UML/OCLに記述された時間 QoS の階層的検証手法の提案
Hierarchical Model Checking to Ensure Timeliness QoS Described in UML/OCL
UML　OCL　ニ　キジュツ　サレタ　ジカン　Qos　ノ　カイソウテキ　ケンショウ　シュホウ　ノ　テイアン
著者
著者名
長井, 栄吾 ; ナガイ, エイゴ ; Nagai, Eigo
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
著者名
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
キーワード等
分散実時間アプリケーション
時間QoS
モデル検査
UPPAAL
形式的検証
Real-time Distributed System
Timeliness QoS
Model Checking
Formal Verification
抄録
分散実時間アプリケーションにおいては,ユーザに対して提供されるQoS(Quality of Service)を保証することがきわめて重要である.特に,時間QoSに対する要求の保証が重要視されている.本稿では,UML/OCLに記述された時間QoSを多段階かつ階層的に検証する方法を提案する.コンポーネントの時間的振る舞いを時間オートマントで抽象化した抽象QoSモデルを利用することで,時間QoSを多段階かつ階層的に形式的に保証する.これにより,状態爆発など既存の手法が抱える問題を解消し,効率的に時間QoSの整合性の判定が可能となる.提案手法をUPPAALを用いて例題に適用した結果,検証時間の観点から見て有用であることがわかった.
Distributed Real-time application should generally ensure QoS (Quality of Service) providing to end-users. In particular, to ensure timeliness QoS is important. The paper proposes a hierarchical approach to verify formally timeliness QoS for UML/OCL specification of real-time applications. The method uses an abstract QoS model which models abstract behavior of a given component in a timed automaton. Also the method can be applied recursively along with depth of component hierarchy. Thus, the method avoids the state-explosion problem and verify effectively the timeliness QoS properties. Applying the proposed method to an example with UPPAAL, one of the famous model checkers, finds the method is useful.
出版者
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻(号)
106(202)
ページ
13-18
刊行年月
2006-07-28
言語
日本語
ハンドルURL
https://hdl.handle.net/11094/27421
PISSN
09135685
NCID
AN10013287
アクセス権
open access
権利情報
Copyright © 2006 IEICE
本文データはCiNiiから複製したものである
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article