earticle

영어

UML 2 communication diagrams are a well known graphical language and are widely used to specify the dynamic behaviors of transaction-oriented systems. However, communication diagrams are expressed in a semi-formal modeling language and need a well-dened formal semantic base for their notations. This formalization enables analysis and veri- cation tasks. Many eorts have been made to transform sequence diagrams into formal representations including Petri nets, but very few works have been proposed for transforming communication diagrams into formal methods, and none, to our knowledge, has used Buchi automata. Buchi automata are a mathematical tool allowing formal specication of the system dynamics and they are commonly used in Model Checking based on automata theory. For these reasons, in this paper, we present a transformation approach that consists of a source metamodel for UML 2 communication diagrams, a target metamodel for Buchi automata and transformation rules. This approach has been implemented using Atlas Transformation Language (ATL). A Cellular Phone System is considered, as a case study. Keywords UML 2, Communication diagrams, Buchi automata, Model checking, Model transformation, Metamodeling, Transformation rules, ATL