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, 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.
Type de document :
Communication dans un congrès
Kung-Kiu Lau and Richard Banach. 7th International Conference on Formal Engineering Methods - ICFEM 2005, Nov 2005, Manchester, France. Springer Berlin / Heidelberg, 3785, pp.96-110, 2007, Lecture Notes in Computer Science. 〈10.1007/11576280〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00329938
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 13 octobre 2008 - 16:40:01
Dernière modification le : jeudi 15 février 2018 - 08:48:09

Identifiants

Citation

Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard. How Symbolic Animation can help designing an Efficient Formal Model. Kung-Kiu Lau and Richard Banach. 7th International Conference on Formal Engineering Methods - ICFEM 2005, Nov 2005, Manchester, France. Springer Berlin / Heidelberg, 3785, pp.96-110, 2007, Lecture Notes in Computer Science. 〈10.1007/11576280〉. 〈inria-00329938〉

Partager

Métriques

Consultations de la notice

212