ATL Use Case - Compiling a new formal verification language to LOTOS (ISO 8807)
In this use case, we translate FIACRE programs into LOTOS (ISO 8807) programs. This work is the result of the cooperation of two INRIA teams: ATLAS (Nantes), and VASY (Grenoble), in the context of the OpenEmbeDD project.
Keywords
LOTOS, ISO 8807, FIACRE, formal verification, model-checking. |
Overview
FIACRE (french acronym of: Format Intermédiaire pour les Architectures de Composants Répartis Embarqués, meaning: Intermediate Format for the Architectures of Embedded Distributed Components) is a new intermediate language for the formal description and verification of asynchronous concurrent systems. In this work, we define a compiler from FIACRE to LOTOS (Language Of Temporal Ordering Specification, ISO 8807) using Model Engineering techniques. The output of this compiler can then be verified using the CADP toolbox. The abstract syntax of each language is defined in KM3, and the concrete syntax in TCS. The translation from FIACRE to LOTOS is defined as an ATL model-to-model transformation. The current version is able to translate FIACRE types (e.g., enumerations, intervals, arrays), which definitions are relatively concise, into equivalent LOTOS types, which definitions are typically more verbose. For instance, the sample FIACRE program given in Figure 1 is automatically transformed into the LOTOS program given in Figure 2. Note that both programs are presented as screenshots of TGE (Textual Generic Editor), the TCS-based editor. This shows that once the concrete syntax of a language has been defined in TCS, TGE can be used to automatically provide a language-specific editor.
Although only types are transformed at the current time, the definitions (abstract and concrete syntaxes) of FIACRE and LOTOS cover larger parts of the languages. For instance, Figure 3 shows how TGE can edit one of the LOTOS examples.
We also created a web service to use this transformation scenario, so that it can be tested and used without having to install Eclipse. You can see below a sample output of this web service invoked on the same sample FIACRE program as used in Figure 1. Compilaton of a simple FIACRE enumeration into a LOTOS type with the FIACRE2LOTOS web service Source: FIACRE Model1 type test is 2 enum a, b, c end Target: LOTOS Model1 (* ---------------------------------------------------------------------------- *) 2 (* Author: FIACRE2LOTOS.atl *) 3 (* Automatically generated code *) 4 (* ---------------------------------------------------------------------------- *) 5 specification unnamed : noexit 6 7 type test is Boolean 8 sorts 9 test 10 opns 11 a (*! constructor *) 12 , b (*! constructor *) 13 , c (*! constructor *) 14 : -> test 15 _eq_, _neq_ : test, test -> Bool 16 eqns 17 forall x, y : test 18 19 ofsort Bool 20 x = y => x eq y = true; 21 x eq y = false; 22 x neq y = not(x eq y); 23 endtype 24 behaviour 25 26 27 28 endspec |
Related Use Cases
None at the current time. |
Download
FIACRE Language Project |
Language Project defining FIACRE: KM3 metamodel, TCS model, and FIACRE2LOTOS.atl compiler. |
LOTOS Language Project |
Language Project defining LOTOS: KM3 metamodel, and TCS model. |
Acknowledgement
The present work is being supported by the OpenEmbeDD project. We would like to thank Marc Pantel (Toulouse) from the TopCased project, and Christian Attiogbé from the COLOSS team (Nantes) for their advice. |
General Information
- September 2007
- By Frédéric Jouault (INRIA ATLAS), and Frédéric Lang (INRIA VASY)
Please, ask your questions on the M2M newsgroup