An Approach to UML Consistency Checking Based on Compositional Semantics

An Approach to UML Consistency Checking Based on Compositional Semantics

Messaoudi Nabil (Misc laboratory University Abdel Hamid Mehri Constatntine II, Constantine, Algeria & University Abbes Laghrour, Khenchela, Algeria), Allaoua Chaoui (Misc Laboratory, University Abdel Hamid Mehri, Constantine II, Constantine, Algeria) and Mohamed Bettaz (Philadelphia University, Amman, Jordan)
DOI: 10.4018/IJERTCS.2017070101


One of the ways to specify dynamic behavior in UML is to model interactions between objects with sequence diagrams, and model the behavior of each object with state machines. In this context, the problem of ensuring consistency between the sequence diagrams and state machines may arise. To verify consistency, the authors propose an approach based on compositions of Büchi automata which allow us to capture the evolution of each object among the lifeline. This paper focuses on UML modeling and verification methods and bridges the gap between theoretical studies on formal semantics and practical studies to implement languages through model transformations. The transformations include basic interactions, state invariants, strict and weak sequencing, and alternative interaction fragments. Ultimately, the results of the transformations are integrated into the Spin model checker as a never claim property. The authors use the Automatic Gate Controller Railway (AGCR) as an example to illustrate their approach.
Article Preview


The Unified Object Modeling Language (UML) proposes many views in the form of diagrams to model the same system, but it does not have a methodology which clearly specifies how to use these multiple views; it doesn’t define a formal semantics that links these views (Object Management Group, 2005). In particular, UML’s interaction diagrams in the current metamodel do not have an operational semantics which formally specifies how such diagrams are constructed (Planas, 2009; Liu et al., 2013; Chama et al., 2015; Messaoudi et al., 2016). The current semantics of UML in Model Driven Engineering (MDE) comprises a metamodel which describes the notation and informal textual annotations. The Object Constraint Language (OCL) provides the only way to complete the metamodel’s syntactic rules. However, the powerful expressions of OCL are not sufficient to check consistencies in the dynamic behavior because they cannot change the properties of objects and variables (Object Management Group, 2005); a model can contain behaviors which were not anticipated by the designer. They only allow us to check syntactic diagrams. As a result, the formulation of formal models such as automata for predicting inconsistencies is imperative.

If the interactions describe finite-state systems (Elaasar & Briand, 2004), it is sufficient to use automata that accept only finite words. However, interactions can potentially create nonfinite words (Planas, 2009; Elaasar & Briand, 2004). The algorithm built into SPIN (Knapp, 2008) to produce never claims from linear temporal logic (LTL) formulas is ineffective for communications which specify more than five or so actions (Cengarle & Knapp, 2006). This motivates the use of -automata, such as Büchi automata, to describe interactions in Unified Modeling Language 2 Sequence Diagrams (UML2SDs). As is well known, a UML2SD represents communication between a set of processes each of which is a UML state machine. A necessary condition is that each process can wait infinitely long to consume a message from another process, and this implies that it is necessary to self-loop in each state. Thus, a simple finite state machine (FSM) cannot represent the behavior of a UML2SD, and Büchi automata are necessary.

The first problem we encounter when developing the transformation rules is the lack of a precise semantics, which makes the validation impossible. The second problem is that, unfortunately, the definition of UML interactions only concerns the scheduling of messages and doesn’t specify anything about the actions of objects (Cardoso& Sibertin-Blanc, 2001). In this regard, several works have attempted to couple UML interactions with formal models (automata, Petri-nets, Pi-calculus and timed automata) in order to check for deadlock and the liveness of the models. These works indicate how to translate interactions into formal models, depending on the characteristics of the message. However, most of the proposed semantics do not specify how to generate all corresponding formal models. For this purpose, it is appropriate to provide a compositional semantics for UML2SDs and endow the objects with events which permit the generation of automata. This work uses synchronized sections whenever combined fragments are entered, which enables correct treatment of the interleaving of combined fragments. The result offing automaton is then textually transformed into Process Meta Language (Promela) code, which will play the role of a never claim property for the model checker SPIN (Holzman, 2003). We have therefore implemented a set of formalized mapping rules using the ATL the ATLAS Transformation Language; language. OCL (Object Management Group, 2005) constraints is used to describe constraints on the source model and the target model in order to ensure that the target model is the correct transformation result for the source model.

Complete Article List

Search this Journal:
Open Access Articles: Forthcoming
Volume 10: 4 Issues (2019): 1 Released, 3 Forthcoming
Volume 9: 2 Issues (2018)
Volume 8: 2 Issues (2017)
Volume 7: 2 Issues (2016)
Volume 6: 2 Issues (2015)
Volume 5: 4 Issues (2014)
Volume 4: 4 Issues (2013)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing