ATL Use Case - Compiling a new formal verification language to LOTOS (ISO 8807)

ATL Logo

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.



Figure 1. Simple FIACRE enumeration as seen in TGE



Figure 2. LOTOS type generated from the simple FIACRE enumeration (click picture for larger version)

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.



Figure 3. The bitalt.lotos LOTOS example edited in TGE (click picture for larger version)

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 Model

1	type test is
2	    enum a, b, c end


Target: LOTOS Model

1	(* ---------------------------------------------------------------------------- *)
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