Equivalence Checker for the Papyrus-RT framework

Organisation:	IRIT and University of Toulouse (FRANCE) Queen's University, Kingston (CANADA)
Functionality:	Equivalence checking of UML-RT models
Tools used:	ATL (ATLAS Transformation Language) CADP (Construction and Analysis of Distributed Processes) Eclipse Papyrus-RT
Period:	2017
Description:	Gradually adding fonctionality is an approach to master the complexity of embedded systems. In the context of Model-Driven Development, these incremental additions are often performed as refinement steps, where an abstract model is refined to a more detailed model. This tool provides developers with a formal check that such a refinement step preserves the semantics, automatically checking the equivalence of the underlying LTSs (Labeled Transition Systems). Concrectly, the authors provide a transformation from UML-RT models to LNT, implemented using 18 ATL (ATLAS Transformation Language) rules and 11 helpers. As ATL generates a model-to-model transformation, an XText grammar of LNT has been developed. This has the double advantage of a smooth integration of the transformation into the Eclipse platform of Papyrus-RT, and the automatic availability of a smart editor for LNT. Finally, the equivalence check is implemented as an SVL script, hiding those actions present only in the refinded model, and checking for branching bisimulation and generating a diagnostics trace, which can be inspected using the OCIS interactive step-by-step simulator. The framework has been applied to validate the so-called summary state abstraction pattern, where a so-called glass state is refined to contain several states and transitions.
Conclusions:	Translating UML-RT into LNT is feasible using ATL transformation rules, bridging the worlds of model-driven engineering and formal methods.
Publications:	[Oliveira-Dingel-17] Raquel Oliveira and Jürgen Dingel. "Supporting Model Refinement with Equivalence Checking in the Context of Model-Driven Engineering with UML-RT". Proceedings of the 14th Workshop on Model Engineering, Verification and Validation (MoDeVVa 2017), Austin, Texas, USA, pages 307-314, CEUR, September 2017. Available on-line at: http://ceur-ws.org/Vol-2019/modevva_2.pdf or from the CADP Web site in PDF or PostScript
Contact:	Raquel Oliveira ARGOS team IRIT and Univ. Toulouse 118, Route de Narbonne F-31062 Toulouse Cedex 9 FRANCE Tel: +33 (0)5 61 55 69 46 Email: Raquel.Oliveira at irit.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page