Manuals
Tutorials
-
A simple Fiacre tutorial, for starters
frac and tina howto
A Fiacre primer (in progress)
H-Fiacre -- Hippo extensions and usage
Some introductory Fiacre examples:
| abp.fcr | Alternating bit protocol | |
| fischer.fcr | Fischer mutual exclusion algorithm | |
| peterson.fcr | Peterson mutual exclusion algorithm with 2 sites | |
| trains4.fcr | Level-crossing example with 4 trains | |
| bridge.fcr | Bridge puzzle | |
| sokoban.fcr | Sokoban example game |
Some case studies:
Fiacre reference
-
From Fiacre V2 to Fiacre V3:
Summarizes the changes from Fiacre V2 to Fiacre V3; including a description of fiacre functions;
-
Information on the older Fiacre V2 can be found here.
Papers and reports
[1] B.Berthomieu , J.P.Bodeveix , P.Farail , M.Filali , H.Garavel , P.Gaufillet , F.Lang , F.Vernadat, Fiacre: an intermediate language for model verification in the TOPCASED environment. Embedded Real Time Software and Systems (ERTS2 2008). [ pdf]
[2] B.Berthomieu , J.P.Bodeveix , M.Filali , H.Garavel , F.Lang , F.Peres , R.Saad , J.Stoecker , F.Vernadat, The syntax and semantics of FIACRE. Projet ANR05RNTL03101 OpenEmbeDD 2009 [pdf]
[3] B. Berthomieu, H. Garavel, F. Lang and F. Vernadat, Verifying Dynamic Properties of Industrial Critical Systems Using TOPCASED/FIACRE,
ERCIM NEWS, Special Issue on Safety-Critical Software, October 2008. [web][pdf]
[4] B.Berthomieu , J.P.Bodeveix , C.Chaudet , S.Dal Zilio , M.Filali , F.Vernadat, Formal verification of AADL specifications in the topcased environment. Reliable Software Technologies - Ada Europe 2009. [pdf]
[5] B.Berthomieu , J.P.Bodeveix , S.Dal Zilio , M.Filali , M.Pantel , F.Vernadat, Langage intermédiaire et transformations de modèles pour le développement de systèmes temps-réel: retour d'expérience sur la chaîne de vérification formelle Fiacre. IDM 2010. [pdf]
[6] T.Correa , L.B.Becker , J.P.Bodeveix , J.M.Farines , M.Filali , F.Vernadat, Verification based development process for embedded systems.
Embedded Real Time Software and Systems (ERTS2 2010). [pdf]
[7] B.Berthomieu, J.P.Bodeveix, S. Dal Zilio, P. Dissaux, M.Filali, P. Gaufillet, S.Heim, F.Vernadat, Formal Verification of AADL models with Fiacre and Tina. Embedded Real Time Software and Systems (ERTS2 2010). [pdf]
[8] T.Correa , L.B.Becker , J.M.Farines , J.P.Bodeveix , M.Filali , F.Vernadat, Supporting the design of safety critical systems using AADL.
(ICECCS'2010). [pdf]
[9] B.Berthomieu , J.P.Bodeveix , S.Dal Zilio , M.Filali , F.Vernadat, Vérification formelle de spécifications AADL via FIACRE. Ecole d'Eté Temps Réel (ETR'11). [pdf]