|
|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 [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 |
| 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 |