Towards modelling obligations in Event-B

J. Bicarregui, A. Arenas, Benjamin Aziz, P. Massonet, C. Ponsard

Research output: Contribution to conferencePaperpeer-review

88 Downloads (Pure)

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.
Original languageEnglish
Publication statusPublished - 16 Sep 2008
EventABZ 2008 - London
Duration: 16 Sep 200818 Sep 2008

Conference

ConferenceABZ 2008
CityLondon
Period16/09/0818/09/08

Fingerprint

Dive into the research topics of 'Towards modelling obligations in Event-B'. Together they form a unique fingerprint.

Cite this