Liberalising Event B without changing it

dc.contributor.authorReeves, Steveen_US
dc.contributor.authorStreader, Daviden_US
dc.date.accessioned2008-03-19T04:58:15Z
dc.date.available2007-05-30en_US
dc.date.available2008-03-19T04:58:15Z
dc.date.issued2006-07-01en_US
dc.description.abstractWe 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.mimetypeapplication/pdf
dc.identifier.citationReeves, 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.urihttps://hdl.handle.net/10289/48
dc.language.isoen
dc.publisherDepartment of Computer Science, University of Waikatoen_NZ
dc.subjectprocess refinementen_US
dc.subjectautomatic verificationen_US
dc.subjectframe refinementen_US
dc.subjectEvent Ben_US
dc.titleLiberalising Event B without changing iten_US
dc.typeWorking Paperen_US
dspace.entity.typePublication
pubs.place-of-publicationHamiltonen_NZ
uow.relation.series07/2006en_NZ

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
content.pdf
Size:
144.49 KB
Format:
Adobe Portable Document Format