Database of Research Tools Developed Using CADP

The FLAC Fiacre to LOTOS Compiler

Organisation: INRIA (FRANCE)

Functionality: Transformation from FIACRE descriptions to LOTOS.

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

Period: 2011

Description: FIACRE (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués) is a formal intermediate model to represent the behavioural and timing aspects of systems (in particular embedded and distributed systems) for formal verification and simulation purposes. Fiacre embeds the notions of process, to describe the behaviour of sequential components, and of composition of processes communicating through ports.

FIACRE was designed in the framework of projects dealing with model-driven engineering. It is designed both as the target language of model transformation engines from various models such as SDL or UML, and as the source language of compilers into the targeted verification toolboxes, namely CADP and TINA in the first step. It was primarily inspired from two works, namely V-Cotre and NTIF, as well as decades of research on concurrency theory and real-time systems theory.

FLAC is a compiler from FIACRE 2.0 into the language LOTOS. This enables FIACRE descriptions to be verified using CADP. FLAC was developed in SML, principally by Xavier Clerc and Frederic Lang in the framework of the colaborative projects OpenEmbeDD and TOPCASED.



Conclusions: The source code of the FLAC compiler is publicly available on-line from the INRIA Forge at: https://gforge.inria.fr/projects/fiacre-compil

FLAC was used successfully to verify an Air Traffic Control Subsystem, described at: http://cadp.inria.fr/case-studies/09-l-atc.html

Publications: [Berthomieu-Bodeveix-Farail-et-al-08] Bernard Berthomieu , Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gaufillet, Frederic Lang, and Francois Vernadat. "Fiacre: an intermediate language for model verification in the TOPCASED environment". Proceedings of Embedded Real Time Software and Systems ERTS'08, 2008.
Available on-line at: https://hal.inria.fr/inria-00262442
or from the CADP Web site in PDF or PostScript

[Berthomieu-Garavel-Lang-Vernadat-08] Bernard Berthomieu, Hubert Garavel, Frederic Lang and Francois Vernadat. "Verifying Dynamic Properties of Industrial Critical Systems Using TOPCASED/FIACRE". In ERCIM NEWS, Special Issue on Safety-Critical Software, October 2008.
Available on-line at: http://ercim-news.ercim.eu/en75/special/verifying-dynamic-properties-of-industrial-critical-systems-using-topcasedfiacre

[Berthomieu-Bodeveix-Filali-et-al-09] Bernard Berthomieu , Jean-Paul Bodeveix, Mamoun Filali, Hubert Garavel, Frederic Lang, Florent Peres, Rodrigo Saad, Jan Stoecker, and Francois Vernadat. "The syntax and semantics of FIACRE". Version 1.0 alpha. Projet ANR 05 RNTL 03101 OpenEmbeDD, 2009.
Available on-line at: http://homepages.laas.fr/bernard/fiacre/1.0alpha/doc/fiacre.pdf
or from the CADP Web site in PDF or PostScript
Contact:
Frederic Lang
655, avenue de l'Europe
Montbonnot
38334 St Ismier Cedex
FRANCE
Fax: +33 476 61 52 00
Email: cadp@inria.fr



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


Last modified: Thu Feb 11 12:23:11 2021.


Back to the CADP research tools page