Event-B does not provide specific support for the modelling of problems that require some structuring, such as, local variables or sequential ordering of events. All variables need to be declared globally and sequential ordering of events can only be achieved by abstract program counters. This has two unfortunate consequences: such models become less comprehensible — we have to infer sequential ordering from the use of program counters; proof obligation generation does not consider ordering — generating too many proof obligations (although these are usually trivially discharged). In this article we propose a method for specifying structured models avoiding, in particular, the use of abstract program counters. It uses a notation that mainly serves to drive proof obligation generation. However, the notation also describes the structure of a model explicitly. A corresponding graphical notation is introduced that visualises the structure of a model.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Hallerstede10,
author = {Stefan Hallerstede},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {Structured Event-B Models and Proofs},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {273--286},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_21},
doi = {10.1007/978-3-642-11811-1\_21},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/Hallerstede10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}