Database of Research Tools Developed Using CADP

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 our FTP 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


Last modified: Tue Apr 2 16:40:14 2019.


Back to the CADP research tools page