Reeves, SteveStreader, David2008-03-192007-04-292008-03-192006-07-01Reeves, 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.https://hdl.handle.net/10289/89We 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.application/pdfenprocess refinementEvent BLive BSafe BLSBWorking Paper