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 the CADP Web 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 |