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)

[img]
Preview
PDF
SCHNEIDER_stepwise_refinement_2011.pdf

Download (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
Depositing User: Melanie Hughes
Date Deposited: 17 Mar 2011 11:57
Last Modified: 23 Sep 2013 18:40
URI: http://epubs.surrey.ac.uk/id/eprint/2800

Actions (login required)

View Item View Item

Downloads

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