资 源 简 介
DFT-generator, a small tool to generate Deadlock-Freeness Theorems 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 theorems necessary to prove that a model is free of deadlocks.
