Loading...
Thumbnail Image
Item

Liberalising Event B without changing it

Abstract
We transfer a process algebraic notion of refinement to the B method by using the well-known bridge between the relational semantics underlying the B machines and the labelled transition system semantics of processes. Thus we define delta refinement on Event B systems. We then apply this new refinement to a problem from the literature that previously could only be solved by retrenchment.
Type
Working Paper
Type of thesis
Series
Citation
Reeves, S., & Streader, D. (2006). Liberalising Event B without changing it. (Working paper series. University of Waikato, Department of Computer Science. No. 07/2006). Hamilton, New Zealand: University of Waikato.
Date
2006-07-01
Publisher
Department of Computer Science, University of Waikato
Degree
Supervisors
Rights