The Behavioural Semantics of Event-B Re finement

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