| dc.contributor.author | Reeves, Steve | en_US |
| dc.contributor.author | Streader, David | en_US |
| dc.date.accessioned | 2008-03-19T04:58:34Z | |
| dc.date.available | 2007-04-29 | en_US |
| dc.date.available | 2008-03-19T04:58:34Z | |
| dc.date.issued | 2006-07-01 | en_US |
| dc.identifier.citation | 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. | en_US |
| dc.identifier.uri | https://hdl.handle.net/10289/89 | |
| dc.description.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. | en_US |
| dc.format.mimetype | application/pdf | |
| dc.language.iso | en | |
| dc.publisher | Department of Computer Science, University of Waikato | en_NZ |
| dc.subject | process refinement | en_US |
| dc.subject | Event B | en_US |
| dc.subject | Live B | en_US |
| dc.subject | Safe B | en_US |
| dc.subject | LSB | en_US |
| dc.title | LSB - Live and Safe B: Alternative semantics for Event B | en_US |
| dc.type | Working Paper | en_US |
| uow.relation.series | 08/2006 | en_NZ |
| pubs.elements-id | 53348 | |
