Database of Research Tools Developed Using CADP

SLCO Language Transformation Environment

Organisation: Eindhoven University of Technology (THE NETHERLANDS)

Functionality: Transformation from DSL descriptions to LTSs.

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

Period: 2011

Description: Domain-Specific Languages (DSLs) and model transformations are the basic concepts in model driven engineering. A DSL is a language that offers, through appropriate notations and abstractions, expressive power focused on, and usually restricted to, a particular problem domain. A formal definition of the semantics of a DSL is an essential prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. The Simple Language of Communicating Objects (SLCO) provides constructs for specifying systems consisting of objects that operate in parallel and communicate with each other. The structure of a system is modeled using classes and their behavior is modeled by state machines.

For automated analysis purposes, the SLCO language is translated to a simple language for the representation of Labeled Transition Systems (LTSs). This provides a gateway to various tools supporting LTSs, such as CADP, for manipulation, visualization, and verification of SLCO models. The language transformations from SLCO to LTS are defined and implemented in the ASF+SDF meta-environment, which has the ability to parse arbitrary context-free languages and to generate command-line tools that can efficiently execute transformations.

Conclusions: Transforming DSL models to a common description format makes it possible to verify properties of models using existing tools, without additional effort. Another benefit of this approach is the following: the implementation of the transformations from SLCO models to LTSs gives a prototype of the semantics of SLCO. Based on the conditional rewrite rules which form the core of this transformation, the formal operational semantics of the language can be defined. Although the environment is built around SLCO, the same methodology can be applied to other DSLs.

Publications: [Andova-vandenBrand-Engelen-11] Suzana Andova, Mark van den Brand, and Luc Engelen. "Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models". Proceedings of the 2nd International Workshop on Algebraic Methods in Model-Based Software Engineering AMMSE'2011, EPTCS vol. 56, pages 65-79, 2011.
Available on-line at: http://arxiv.org/PS_cache/arxiv/pdf/1107/1107.0067v1.pdf
or from our FTP site in PDF or PostScript

Contact:
Suzana Andova
Department of Mathematics and Computer Science
Eindhoven University of Technology
Den Dolech 2
NL-5612 AZ Eindhoven
The Netherlands
Tel: +31 40 2475089
Fax: +31 40 2475404
Email: s.andova@tue.nl



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page