The Behavioural Semantics of Event-B Re finement

Schneider, SA, Treharne, HE and Wehrheim, H (2014) The Behavioural Semantics of Event-B Re finement Formal Aspects of Computing: applicable formal methods, 26. pp. 251-280.

Preview	Text facsSTW14.pdf - Accepted version Manuscript Available under License : See the attached licence file. Download (548kB) | Preview
Preview	Text (licence) SRI_deposit_agreement.pdf Available under License : See the attached licence file. Download (33kB) | Preview

Abstract

Event-B provides a flexible framework for stepwise system development via re finement. The framework supports steps for (a) re fining 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 refi nement 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 justifi cation has previously been given for the application of these rules in a re finement chain. Behavioural semantics expresses a clear relationship between the first and last machines in a re finement chain. The framework we present provides a coherent justi fication for Abrial's approach to re finement 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 refi nement, 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 de fine a CSP semantics for Event-B and show how the di fferent forms of Event-B refi nement can be captured as CSP re finement. It turns out that the appropriate CSP refi nement 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
Divisions :	Faculty of Engineering and Physical Sciences > Computing Science
Authors :	Name Email ORCID Schneider, SA Treharne, HE Wehrheim, H
Date :	13 March 2014
Additional Information :	The original publication is available at http://www.springerlink.com
Depositing User :	Symplectic Elements
Date Deposited :	15 Apr 2014 16:02
Last Modified :	13 Mar 2015 02:08
URI:	http://epubs.surrey.ac.uk/id/eprint/805394

Actions (login required)

View Item

Downloads