ePubs
The open archive for STFC research publications
Home
About ePubs
Content Policies
News
Help
Privacy/Cookies
Contact ePubs
Full Record Details
Persistent URL
http://purl.org/net/epubs/work/43601
Record Status
Checked
Record Id
43601
Title
Towards modelling obligations in Event-B
Contributors
J C Bicarregui (STFC Rutherford Appleton Lab.)
,
A E Arenas (STFC Rutherford Appleton Lab.)
,
B Aziz (STFC Rutherford Appleton Lab.)
,
P Massonet (CETIC)
,
C Ponsard (CETIC)
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
Obligations
,
Engineering
,
Event-B
Funding Information
EU
Related Research Object(s):
48911766
Licence Information:
Language
English (EN)
Type
Details
URI(s)
Local file(s)
Year
Paper In Conference Proceedings
In International Conference of ASM, B and Z Users (ABZ 2008), London, UK, 16-18 Sept 2008, (2008): 181-194.
http://dx.doi.org…978-3-540-87603-8_15
2008
Showing record 1 of 1
Recent Additions
Browse Organisations
Browse Journals/Series
Login to add & manage publications and access information for OA publishing
Username:
Password:
Useful Links
Chadwick & RAL Libraries
Jisc Open Policy Finder
Journal Checker Tool
Google Scholar