University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Stepwise Refinement in Event-B CSP. Part 1: Safety

Schneider, Steve, Treharne, Helen and Wehrheim, Heike (2011) Stepwise Refinement in Event-B CSP. Part 1: Safety Technical Report. Department of Computing, University of Surrey. (Unpublished)


Download (625kB)


This technical report provides the CSP semantic basis for stepwise refinement in Event-B!CSP. It provides the foundation for combining Event- B machines with CSP control processes in the context of refinement. A number of proof rules are presented which are sufficient to establish refinement of an Event-B!CSP combination. This report focuses on traces, both finite and infinite, which allows consideration of safety specifications and also consideration of divergence-freedom. Several refinement steps in Event-B!CSP in the development of a simple bounded retransmission protocol are presented to illustrate the approach.

Item Type: Monograph (Technical Report)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Wehrheim, Heike
Date : March 2011
Additional Information : Copyright 2011 The Authors
Depositing User : Melanie Hughes
Date Deposited : 17 Mar 2011 11:57
Last Modified : 16 Jan 2019 16:25

Actions (login required)

View Item View Item


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