DIXIT: a Graphical Toolkit for Predicate Abstractions

Loïc Fejoz 1 Dominique Méry 1 Stephan Merz 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We describe a toolkit to support the use of predicate diagrams, a representation of predicate abstractions that includes annotations for proving liveness properties. Centered around a graphical editor for drawing predicate diagrams, proof obligations for proving correctness of the abstraction w.r.t. TLA+ system specifications can be generated, correctness properties expressed in temporal logic can be verified by model checking, and counterexamples can be visualized. The toolkit also supports stepwise development of systems, based on a notion of refinement of predicate diagrams.
Document type :
Conference papers
Ramesh Bharadwaj and Supratik Mukhopadhyay. Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Apr 2005, Edinburgh / U.K., pp.39-48, 2005
Liste complète des métadonnées


https://hal.inria.fr/inria-00000767
Contributor : Stephan Merz <>
Submitted on : Thursday, November 17, 2005 - 12:28:02 PM
Last modification on : Tuesday, December 13, 2016 - 3:45:06 PM
Document(s) archivé(s) le : Friday, April 2, 2010 - 7:33:19 PM

Identifiers

  • HAL Id : inria-00000767, version 1

Collections

Citation

Loïc Fejoz, Dominique Méry, Stephan Merz. DIXIT: a Graphical Toolkit for Predicate Abstractions. Ramesh Bharadwaj and Supratik Mukhopadhyay. Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Apr 2005, Edinburgh / U.K., pp.39-48, 2005. <inria-00000767>

Share

Metrics

Record views

209

Document downloads

146