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. © 2004 Elsevier B.V. All rights reserved.

Proving and debugging set-based specifications / Couchot, J. -F.; Dadeau, F.; Deharbe, D.; Giorgetti, A.; Ranise, S.. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 95:(2004), pp. 189-208. (Intervento presentato al convegno Brazilian Workshop on Formal Methods tenutosi a Campina Grande, bra nel 2003) [10.1016/j.entcs.2004.04.012].

Proving and debugging set-based specifications

Ranise S.
2004-01-01

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. © 2004 Elsevier B.V. All rights reserved.
2004
Proceedings of the Brazilian Workshop on Formal Methods
United States
ELSEVIER
Couchot, J. -F.; Dadeau, F.; Deharbe, D.; Giorgetti, A.; Ranise, S.
Proving and debugging set-based specifications / Couchot, J. -F.; Dadeau, F.; Deharbe, D.; Giorgetti, A.; Ranise, S.. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 95:(2004), pp. 189-208. (Intervento presentato al convegno Brazilian Workshop on Formal Methods tenutosi a Campina Grande, bra nel 2003) [10.1016/j.entcs.2004.04.012].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/332975
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact