IRIT and University of Toulouse (FRANCE)
Queen's University, Kingston (CANADA)
Equivalence checking of UML-RT models
ATL (ATLAS Transformation Language)
CADP (Construction and Analysis of Distributed Processes)
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.
Translating UML-RT into LNT is feasible using ATL transformation
rules, bridging the worlds of model-driven engineering and formal
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
IRIT and Univ. Toulouse
118, Route de Narbonne
F-31062 Toulouse Cedex 9
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|