LSB - Live and Safe B: Alternative semantics for Event B
Authors
Loading...
Permanent Link
Publisher link
Rights
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.
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.
Type
Series name
Date
Publisher
Department of Computer Science, University of Waikato