University of Surrey

Test tubes in the lab Research in the ATI Dance Research

The Behavioural Semantics of Event-B Refinement

Schneider, SA, Treharne, HE and Wehrheim, H (2012) The Behavioural Semantics of Event-B Refinement Formal Aspects of Computing: applicable formal methods. ? - ?. ISSN 0934-5043

[img] PDF (deleted)
facs-refine11.pdf
Restricted to Repository staff only
Available under License : See the attached licence file.

Download (535Kb)
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf

Download (32Kb)
[img] ["document_typename_application/force-download" not defined] (deleted)
facs-refine11.pdf
Restricted to Repository staff only
Available under License : See the attached licence file.

Download (535Kb)
[img]
Preview
["document_typename_application/force-download" not defined]
facs-refine11.pdf
Available under License : See the attached licence file.

Download (535Kb)

Abstract

Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can be indicated as convergent (to be made internal) or anticipated (treatment deferred to a later refinement step). All such steps are accompanied with precise proof obligations. However, no behavioural semantics has been provided to validate the proof obligations, and no formal justification has previously been given for the application of these rules in a refinement chain. Behavioural semantics expresses a clear relationship between the first and last machines in a refinement chain. The framework we present provides a coherent justification for Abrial’s approach to refinement in Event-B, and its generalisation to interface extension: adding events to the interface. In this paper, we give a behavioural semantics for Event-B refinement, with a treatment for the first time of splitting events and of anticipated events, adding to the well-understood treatment of convergent events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement. It turns out that the appropriate CSP refinement relationship is influenced by the particular Event-B development strategy taken. We present two such strategies, one allowing, the other disallowing interface extensions.

Item Type: Article
Additional Information: The original publication is available at <a href="http://link.springer.com/article/10.1007%2Fs00165-012-0265-0?LI=true#</a>
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Symplectic Elements
Date Deposited: 30 Nov 2012 10:07
Last Modified: 23 Sep 2013 19:40
URI: http://epubs.surrey.ac.uk/id/eprint/726036

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800