Towards Modelling Obligations in Event-B

Publication
1st International Conference on ASM, B, and Z (ABZ'08)

Abstract

We propose a syntactic extension of Event-B incorporating a limited notion of obligation described by triggers. The trigger of an event is the dual of the guard: when a guard is not true, an event must not occur, whereas when a trigger is true, the event must occur. The obligation imposed by a trigger is interpreted as a constraint on when the other events are permitted. For example, the simplest trigger next, which states that the event must be the next one to be executed when the trigger becomes true, is modelled as an extra guard on each of the other events which prohibits their execution at this time. In this paper we describe the modelling of triggers in Event-B, and analyse refinement and abstract scheduling of triggered events.

Document

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.

Reference

% BibTex
@inproceedings{BicarreguiAAMP08,
  author       = {Juan Bicarregui and
                  Alvaro Arenas and
                  Benjamin Aziz and
                  Philippe Massonet and
                  Christophe Ponsard},
  editor       = {Egon B{\"{o}}rger and
                  Michael J. Butler and
                  Jonathan P. Bowen and
                  Paul Boca},
  title        = {Towards Modelling Obligations in Event-B},
  booktitle    = {Abstract State Machines, {B} and Z, First International Conference,
                  {ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5238},
  pages        = {181--194},
  publisher    = {Springer},
  year         = {2008},
  url          = {https://doi.org/10.1007/978-3-540-87603-8\_15},
  doi          = {10.1007/978-3-540-87603-8\_15},
  timestamp    = {Thu, 14 Oct 2021 10:31:49 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BicarreguiAAMP08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}


Related