An Event-B Plug-in for Creating Deadlock-Freeness TheoremsReport as inadecuate

An Event-B Plug-in for Creating Deadlock-Freeness Theorems - Download this document for free, or read online. Document in PDF available to download.

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.

Keywords : Event-B Deadlock-Freeness Theorem Plug-in

Author: Faqing Yang - Jean-Pierre Jacquot -



Related documents