Stepwise Refinement in Event-B CSP. Part 1: Safety
Tools
Tools
Tools
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)
![[img]](/style/images/fileicons/application_pdf.png)
| PDF 611Kb |
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.
| Item Type: | Monograph (Technical Report) |
|---|---|
| Additional Information: | Copyright 2011 The Authors |
| Divisions: | Faculty of Engineering and Physical Sciences > Computing Science |
| ID Code: | 2800 |
| Deposited By: | Melanie Hughes |
| Deposited On: | 17 Mar 2011 11:57 |
| Last Modified: | 24 Jan 2013 09:10 |
Document Downloads
Repository Staff Only: item control page