Reeves, S., & Streader, D. (2006). LSB - Live and Safe B: Alternative semantics for Event B. (Working paper series. University of Waikato, Department of Computer Science. No. 08/2006). Hamilton, New Zealand: University of Waikato.
Permanent Research Commons link: http://hdl.handle.net/10289/89
We define two lifted, total relation semantics for Event B machines: Safe B for safety-only properties and Live B for liveness properties. The usual Event B proof obligations, Safe, are sufficient to establish Safe B refinement. Satisfying Safe plus a simple additional proof obligation ACT REF is sufficient to establish Live B refinement. The use of lifted, total relations both prevents the ambiguity of the unlifted relational semantics and prevents operations being clairvoyant.
Department of Computer Science, University of Waikato