Proving and Debugging Set-Based Specifications

Jean-François Couchot 1 Frédéric Dadeau 1 David Déharbe 1 Silvio Ranise 1
1 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 : We present a technique to prove invariants of model-based specifications in a fragment of set theory. Proof obligations containing set theory constructs are translated to first-order logic with equality augmented with (an extension of) the theory of arrays with extensionality. The idea underlying the translation is that sets are represented by their characteristic function which, in turn, is encoded by an array of Booleans indexed on the elements of the set. A theorem proving procedure automating the verification of the proof obligations obtained by the translation is described. Furthermore, we discuss how a sub-formula can be extracted from a failed proof attempt and used by a model finder to build a counter-example. To be concrete, we use a B specification of a simple process scheduler on which we illustrate our technique.
Keywords : set-theory first-order logic with equality decision procedures superposition BDDs haRVey
Type de document :
Communication dans un congrès
6th Brazilian Workshop on Formal Methods, May 2004, Campina Grande, Brazil. 95, pp.189-208, 2004, Electronic Notes in Theoretical Computer Science - ENTCS. 〈10.1016/j.entcs.2004.04.012〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00329994
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 13 octobre 2008 - 17:31:43
Dernière modification le : vendredi 6 juillet 2018 - 15:06:09

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LORIA | UNIV-LORRAINE

Citation

Jean-François Couchot, Frédéric Dadeau, David Déharbe, Silvio Ranise. Proving and Debugging Set-Based Specifications. 6th Brazilian Workshop on Formal Methods, May 2004, Campina Grande, Brazil. 95, pp.189-208, 2004, Electronic Notes in Theoretical Computer Science - ENTCS. 〈10.1016/j.entcs.2004.04.012〉. 〈inria-00329994〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

129

Contact


archive-ouverte@inria.fr