How Symbolic Animation can help designing an Efficient Formal Model

Fabrice Bouquet (1, 2) , Frédéric Dadeau (1, 2) , Bruno Legeard (1, 2)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems

This paper presents a non-conventional application of symbolic animation. We propose to assist the modeller in building an efficient formal model, by automatically detecting potential weaknesses or imprecisions in the model. We propose to detect inconsistencies within the formal models written with pre- and postconditions, and to point out unusual model properties, such as a weak invariant or unreachable effects. Our approach is based on constraint solving technologies to perform the animation and to detect the various problems.

Mots clés: symbolic animation; properties detection; weak invariant; strong preconditions; unreachable effects; constraints

Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard. How Symbolic Animation can help designing an Efficient Formal Model. 7th International Conference on Formal Engineering Methods - ICFEM 2005, Nov 2005, Manchester, France. pp.96-110, ⟨10.1007/11576280⟩. ⟨inria-00329938⟩