The Behavioural Semantics of Event-B Refinement

Photograph of Helen Treharne

Helen Treharne

(University of Surrey)

Event-B provides a flexible framework for stepwise system development via refinement. 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. 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. Interestingly the appropriate CSP refinement relationship is influenced by the particular Event-B development strategy taken.
Thursday 15th November 2012, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science