講演名 2010-02-26
UMLシーケンス図における時間制約の記述とその検証(次世代経営情報技術,その他)
安田 佳宏, 新川 芳行,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) UML2.0ではシーケンス図に時間制約の記述が可能となっているが,UML自体にはその検証機能がないため,時間制約の検証は,他のツール等により行う必要がある.本論文では,実時間モデル検証ツールUPPAALにより,UMLシーケンス図の時間制約検証を行う手法について述べる.UPPAALは時間オートマトンを対象とするため,UMLシーケンス図をこの形式に変換すれば,検証が可能となる.本論分では二つの変換手法を提案し,UPPAALでの検証を行った.
抄録(英) In UML2.0, it is possible to describe time constraints in sequence diagrams. However it seems difficult to validate or verify the constraints, since no capability is provided by UML for this verification. Therefore, we need to use appropriate tools that can verify the time constraints. This paper presents a verification process for the time constraints in UML sequence diagrams using UPPAAL. Since UPPAAL is based on timed automata, the sequence diagrams have to be transformed into timed automata. We propse two different transformation rules for the verification.
キーワード(和) UML / シーケンス図 / 時間オートマトン / UPPAAL
キーワード(英)
資料番号 SWIM2009-24
発行日

研究会情報
研究会 SWIM
開催期間 2010/2/19(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Software Interprise Modeling (SWIM)
本文の言語 JPN
タイトル(和) UMLシーケンス図における時間制約の記述とその検証(次世代経営情報技術,その他)
サブタイトル(和)
タイトル(英) Description and Verification of Time Constraints in UML Sequence Diagrams
サブタイトル(和)
キーワード(1)(和/英) UML
キーワード(2)(和/英) シーケンス図
キーワード(3)(和/英) 時間オートマトン
キーワード(4)(和/英) UPPAAL
第 1 著者 氏名(和/英) 安田 佳宏 / Yoshihiro YASUDA
第 1 著者 所属(和/英) 龍谷大学大学院理工学研究科情報メディア学専攻
Department of Science and Engineering, Ryukoku University
第 2 著者 氏名(和/英) 新川 芳行 / Yoshiyuki SHINKAWA
第 2 著者 所属(和/英) 龍谷大学大学院理工学研究科情報メディア学専攻
Department of Science and Engineering, Ryukoku University
発表年月日 2010-02-26
資料番号 SWIM2009-24
巻番号(vol) vol.109
号番号(no) 430
ページ範囲 pp.-
ページ数 6
発行日