講演抄録/キーワード |
講演名 |
2010-06-04 16:30
時間制約が存在するUMLの正当性検証 ○野村将人・新川芳行(龍谷大) SWIM2010-7 |
抄録 |
(和) |
本論文では、モデル検査ツールUPPAALを用いてUMLシーケンス図の正当性を検証する方法について述べる。UPPAALはシステムを時間オートマトンの集合として記述するため、シーケンス図を直接入力することはできない。そこで、シーケンス図を時間オートマトンに変換するための手法を提案した。また、シーケンス図から変換された時間オートマトンに対して、UPPAALを用いてモデル検査を行い、手法の妥当性を確認した。 |
(英) |
This paper discusses a validation process for UML sequence diagrams using a model checking tool UPPAAL. Since UPPAAL deals with the models expressed in the form of timed automata, it cannot validate UML sequence diagrams directly. Therefore, we first define a translation rules from sequence diagrams to timed automata. In addition, a sample application is used to evaluate our validation process. |
キーワード |
(和) |
UML / シーケンス図 / 時間オートマトン / UPPAAL / / / / |
(英) |
UML / Sequence Diagrams / Timed Automata / UPPAAL / / / / |
文献情報 |
信学技報, vol. 110, no. 70, SWIM2010-7, pp. 45-50, 2010年6月. |
資料番号 |
SWIM2010-7 |
発行日 |
2010-05-28 (SWIM) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SWIM2010-7 |