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

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

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

Number of Access:510（2025-12-09 11:09 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27421

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr106_202_013 pdf None 628 KB 80 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
UML/OCLに記述された時間 QoS の階層的検証手法の提案
Hierarchical Model Checking to Ensure Timeliness QoS Described in UML/OCL
UML　OCL　ニ　キジュツ　サレタ　ジカン　Qos　ノ　カイソウテキ　ケンショウ　シュホウ　ノ　テイアン
Creator
CreatorName
長井, 栄吾 ; ナガイ, エイゴ ; Nagai, Eigo
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
分散実時間アプリケーション
時間QoS
モデル検査
UPPAAL
形式的検証
Real-time Distributed System
Timeliness QoS
Model Checking
Formal Verification
Abstract
分散実時間アプリケーションにおいては,ユーザに対して提供される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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
106(202)
Page
13-18
Date of Issued
2006-07-28
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27421
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2006 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article