To appear in EPTCS. A CSP account of Event-B refinement

Event-B provides a flexible framework for stepwise system development via refinement. The frame-work 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 moreover possibly be anticipated or conver-gent. All such steps are accompanied with precise proof obligations. Still, it remains unclear what the exact relationship- in terms of a behaviour-oriented semantics- between an Event-B machine and its refinement is. In this paper, we give a CSP account of Event-B refinement, with a treatment for the first time of splitting events and of anticipated events. To this end, we define a CSP seman-tics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement.