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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata

https://hal.inria.fr/inria-00329938
Contributor : Frédéric Dadeau Connect in order to contact the contributor
Submitted on : Monday, October 13, 2008 - 4:40:01 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM

Links full text

Identifiers

Citation

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⟩

Share

Metrics

Record views

303