Algorithmic Analysis of Event-B in Rewriting Logic

This paper presents a rewriting logic semantics for Event-B, a proof-based formal method for discrete systems modeling. The proposed semantics adequately captures the sources of non-deterministic and concurrent behavior in the language. This semantics also axiomatizes an extension of the language, featuring probabilistic behavior due to probabilistic assignment and choice, and guarded transitions. As a result, many forms of algorithmic verification techniques become accessible for reachability analysis, including temporal logic model checking, as well as probabilistic simulation and statistical model checking. The latter can ensure that specific behavior is present or absent in the system of interest, up to a certain confidence threshold, regardless of the way it operates amid uncertain information, being a useful complement to reachability analysis. This approach takes as input an Event-B specification, maybe annotated with probabilities, and outputs an executable rewrite theory that can be checked against different tools, as illustrated with examples in the paper.