UMLシーケンス図によるビジネスプロセス表現とその検証
1) 龍谷大学理工学研究科
| Abstract | スピードが要求される近年のビジネスプロセス（BP）では、時間制約が重要な要因となる。BPの表記法には様々なものがあるが、情報システムとの適合性を考慮すると、UMLも有力な選択肢となる。UMLには13種類の図（ダイアグラム）があり、このうち時間制約の記述が可能なものはシーケンス図とタイミング図となる。前者がシステムの大域的動作のモデル化に向いているのに対し、後者は局所的動作に適していると考えられる。BPは大域的動作と考えられるため、本論文ではシーケンス図によるBPの記述と、時間制約を含む動作の妥当性検証手法を述べる。UML自身には、この妥当性検証の機能がないため、この部分はUPPAALというモデル検査ツールを用いる。 |
|---|---|
| Recent business processes (BP) need more speed than what they were, and therefore the time constraints are important. Among many kinds of notation, UML is one of the alternatives to be taken into account for the information systems. Although UML provides us with 13 types of diagrams, only the sequence and timing diagrams can express the time constraints. While the former is suitable for modeling the global behavior, the latter focuses on more local behavior. The BP shows global behavior, therefore this paper uses the sequence diagram, and presents how the BP is modeled verified from behavioral viewpoints including time constraints. In this verification, we use the UPPAAL model checker, since UML itself is not capable of verification. | |
| Keywords | 統一モデリング言語，ビジネスプロセス，時間オートマトン |
| UML，Business Process，Timed Automata |
