ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/43601
Record Status Checked
Record Id 43601
Title Toward Modelling Obligations in Event-B
Contributors
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.
Organisation ESC , ESC-IM , STFC
Keywords Engineering , Event-B , Obligations
Funding Information
Related Research Object(s):
Language English (EN)
Type Details URI(s) Local file(s) Year
Paper In Conference Proceedings Lecture Notes in Computer Science, Springer. Is in proceedings of: International Conference of ASM, B and Z Users (ABZ 2008), London, UK, 16-18 Sep 2008. http://dx.doi.org…978-3-540-87603-8_15 2008
Showing record 1 of 1
RCUK
Science and Technology Facilities Council Switchboard: 01793 442000