Skip to Main content Skip to Navigation
Conference papers

How Symbolic Animation can help designing an Efficient Formal Model

Fabrice Bouquet 1, 2 Frédéric Dadeau 1, 2 Bruno Legeard 1, 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Frédéric Dadeau <>
Submitted on : Monday, October 13, 2008 - 4:40:01 PM
Last modification on : Wednesday, October 14, 2020 - 4:07:28 AM

Links full text



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⟩



Record views