Database of Case Studies Achieved Using CADP

Semantics Tuning of UML/SysML

Organisation: IRIT and University of Toulouse (FRANCE)

Method: UML

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded Systems.

Period: 2011

Size: n/a

Description: Model Driven Engineering (MDE) approaches are being adopted in a large number of domains. UML and SysML are two examples of languages used in this context. In the area of embedded software, but not only, one of the reasons the use of models is interesting is that they allow for early verification at model level. The early verification is done using various automation techniques, amongst the most used being model checking techniques. This work aims at increasing the scalability of model checking techniques for these modeling languages by proposing a semantics optimisation approach focused on composite structures, as defined in UML2 and SysML. The existing semantics was optimized based on the observation that in most of the cases, the notions of port, interface, and connector usually present in the hierarchical models of industrial systems, are much simpler that their complex counterparts defined by the UML2 standard.

The alternative, optimized semantics yields equivalent representations of the models in terms of labeled transition systems. This qualitative evaluation of the alternative semantics, as implemented in the OMEGA2 framework, was illustrated on the model of an automated teller machine (ATM), by checking that the two LTSs produced by the standard and alternative semantics are strongly bisimilar, using the CADP toolbox.

Conclusions: Successful applications of formal methods and verification in MDE require a careful analysis of the correlation between the semantics of the model and the actual needs of its application domain. General languages, such as UML, have the huge advantage of being largely known and applicable. However, they often bring an overhead that proves to be critical for model-based verification and validation activities. For the communities using these languages, it may be interesting to set up a repository of semantic variants, which makes explicit the details about the induced restrictions, the sufficient conditions for equivalence with the standard semantics, and the potential gains in terms of various metrics, including simulation and model checking capabilities.

Publications: [Ober-Ober-Dragomir-Aboussoror-11] Ileana Ober, Iulian Ober, Iulia Dragomir, and El Abri Aboussoror. "UML/SysML Semantic Tunings". Innovations in Systems and Software Engineering 7(4):257-264, 2011.
Available on-line at:
Ober Ileana
IRIT, University Paul Sabatier
118, route de Narbonne
F-31062 Toulouse Cedex 9
Tel: +33 (0)5 61 55 74 23
Fax: +33 (0)5 61 55 68 47

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page