The Fiacre Language

 

• Home
• News
• Download
• Docs
• Friends
• Contacts
• Tina
• Fiacre
• Hippo

Topcased

Fiacre development started as a joint work by:

the OLC/CFA, now VerTICS, team of LAAS-CNRS, home of TINA,
the VASY/CONVECS project of INRIA, home of CADP,
the ACADIE team of IRIT,

with initial support from the ACI Fiacre and the Topcased project.

This effort led to the definition of Fiacre V2 and a first generation of verification chains for Fiacre through frac, that compiles Fiacre to TTS descriptions supported by the TINA toolbox, and flac, that compiles Fiacre to LOTOS specifications supported by the CADP toolbox. A meta-model of Fiacre was also produced.

In the Topcased project, Fiacre was to be used as an intermediate language between user level notations like AADL, SDL or UML and the low level descriptions expected by verification tools TINA and CADP. Fiacre code was obtained by model-transformation techniques, making use of the Fiacre metamodel,

CADP

In the framework of Topcased, the VASY/CONVECS project developped flac, a compiler from Fiacre V2 to LOTOS, available at http://gforge.enseeiht.fr.

For information about flac and support of Fiacre by CADP, please contact Frederic.Lang at inria.fr or Hubert.Garavel at inria.fr.

AADL2Fiacre

Following Topcased, Fiacre was put to work in several other projects as an intermediate language for verification of AADL descriptions. These experiments resulted in the AADL2Fiacre chain of tools, compiling AADL specifications into Fiacre descriptions.

For information about the AADL2Fiacre tool chain, please contact Mamoun.Filali at irit.fr or Jean-Paul.Bodeveix at irit.fr.

The AADL2Fiacre experiment prompted the definition of Fiacre V3, a conservative extension of V2 notably supporting functions and supported by frac; the differences between Fiacre V2 and V3 are summarized in this document.

PragmaDev

The PragmaDev company, home of Real Time Developer Studio (RTDS), is experimenting the Fiacre/Tina toolchain for the verification of SDL descriptions. An experimental version of RTDS allows one to translate SDL descriptions into Fiacre descriptions. These Fiacre descriptions, augmented with properties declarations and verification requests, are then model checked using the Tina tools.

A flash demo of the experiment is available at: Model checking with FIACRE.

For information about RTDS and the Fiacre/Tina support, please contact Pragmadev.

OBP

The STIC/IDM team at ENSTA Bretagne is developping OBP-CDL, a tool chain for verification of specifications in a fragment of Fiacre, under context constraints specified in CDL (Context Description Language).

OBP takes as input a context description in CDL and a Fiacre specification, possibly splits the context into an equivalent set of smaller contexts, and returns a set of FIACRE programs each constrained by a context element. OBP leverages existing simulators and model checkers such as TINA or OBP-Explorer.

For information about the OBP-CDL tool chain, please contact Philippe.Dhaussy at ensta-bretagne.fr or Jean-Charles.Roger at ensta-bretagne.fr.