Abstract
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.