Liberalising Event B without changing it
| dc.contributor.author | Reeves, Steve | en_US |
| dc.contributor.author | Streader, David | en_US |
| dc.date.accessioned | 2008-03-19T04:58:15Z | |
| dc.date.available | 2007-05-30 | en_US |
| dc.date.available | 2008-03-19T04:58:15Z | |
| dc.date.issued | 2006-07-01 | en_US |
| dc.description.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. | en_US |
| dc.format.mimetype | application/pdf | |
| dc.identifier.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. | en_US |
| dc.identifier.uri | https://hdl.handle.net/10289/48 | |
| dc.language.iso | en | |
| dc.publisher | Department of Computer Science, University of Waikato | en_NZ |
| dc.subject | process refinement | en_US |
| dc.subject | automatic verification | en_US |
| dc.subject | frame refinement | en_US |
| dc.subject | Event B | en_US |
| dc.title | Liberalising Event B without changing it | en_US |
| dc.type | Working Paper | en_US |
| dspace.entity.type | Publication | |
| pubs.place-of-publication | Hamilton | en_NZ |
| uow.relation.series | 07/2006 | en_NZ |
Files
Original bundle
1 - 1 of 1