TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory
This work provides a theoretical foundation for verifying liveness in Event-B, a key challenge for state-based formal methods, but remains incremental as it builds on existing Event-B logic.
The paper extends Event-B logic to TREBL, a fragment for expressing liveness conditions, and provides sound and relatively complete derivation rules. It shows that for any valid entailment, a derivation exists if the machine is sufficiently refined, with refinements always possible.
The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $φ$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.