An Event-B Plug-in for Creating Deadlock-Freeness Theorems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

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

Jean-Pierre Jacquot
  • Fonction : Auteur
  • PersonId : 835382

Résumé

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.
Fichier principal
Vignette du fichier
sbmf2011shortpapers_submission_7-camera-ready.pdf (96.11 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00623825 , version 1 (15-09-2011)

Identifiants

  • HAL Id : inria-00623825 , version 1

Citer

Faqing Yang, Jean-Pierre Jacquot. An Event-B Plug-in for Creating Deadlock-Freeness Theorems. 14th Brazilian Symposium on Formal Methods, Brazilian Computer Society, Sep 2011, São Paulo, Brazil. ⟨inria-00623825⟩
205 Consultations
263 Téléchargements

Partager

Gmail Facebook X LinkedIn More