An Event-B Plug-in for Creating Deadlock-Freeness Theorems

Faqing Yang 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents DFT-generator, a small tool to generate Deadlock-Freeness Theorems (DFT) in Event-B specifications. Event-B, a companion to the B-method, allows specifiers to model systems and environments with the help states, invariants, and events. Events are guarded generalized substitutions which are fired non-deterministically. Assessing temporal properties such as termination or as non-blocking cycle is then a necessity. To overcome the lack of deadlock checking in the core of Event-B and of its supporting environment, Rodin, we have developed a practical little tool which generates the necessary theorems to prove that a model is free of deadlocks. We explain what are the deadlock theorems, why we need a tool to help generating the theorems, what problems were encountered during development. We conclude on a quick comparison with model-checking.
Type de document :
Communication dans un congrès
14th Brazilian Symposium on Formal Methods, Sep 2011, São Paulo, Brazil. 2011
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger
Contributeur : Faqing Yang <>
Soumis le : jeudi 15 septembre 2011 - 22:47:34
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 23:47:07


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00623825, version 1



Faqing Yang, Jean-Pierre Jacquot. An Event-B Plug-in for Creating Deadlock-Freeness Theorems. 14th Brazilian Symposium on Formal Methods, Sep 2011, São Paulo, Brazil. 2011. 〈inria-00623825〉



Consultations de la notice


Téléchargements de fichiers