Show simple item record  

dc.contributor.authorReeves, Steveen_US
dc.contributor.authorStreader, Daviden_US
dc.date.accessioned2008-03-19T04:58:34Z
dc.date.available2007-04-29en_US
dc.date.available2008-03-19T04:58:34Z
dc.date.issued2006-07-01en_US
dc.identifier.citationReeves, 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.en_US
dc.identifier.urihttps://hdl.handle.net/10289/89
dc.description.abstractWe 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.en_US
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherDepartment of Computer Science, University of Waikatoen_NZ
dc.subjectprocess refinementen_US
dc.subjectEvent Ben_US
dc.subjectLive Ben_US
dc.subjectSafe Ben_US
dc.subjectLSBen_US
dc.titleLSB - Live and Safe B: Alternative semantics for Event Ben_US
dc.typeWorking Paperen_US
uow.relation.series08/2006en_NZ
pubs.elements-id53348


Files in this item

This item appears in the following Collection(s)

Show simple item record