Bibtex Record:
@workingpaper{
Author = {Reeves, S. and Streader, D.},
Title = {LSB - Live and Safe B alternative semantics for Event B},
Publisher = {Department of Computer Science, The University of Waikato},
Number = {08/2006},
Pages = {1-18},
Month = {July},
Abstract = {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.},
Keywords = {Process refinement, Event B, Live B, Safe B, LSB},
URL = {http://www.cs.waikato.ac.nz/pubs/wp/2006/uow-cs-wp-2006-08.pdf},
Year = {2006}
}