University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Bounded Retransmission in Event-B||CSP: A Case Study

Schneider, Steve A., Treharne, Helen and Wehrheim, Heike (2011) Bounded Retransmission in Event-B||CSP: A Case Study Department of Computing, University of Surrey. (Unpublished)

[img]
Preview
PDF
brpTR.pdf

Download (423Kb)

Abstract

Event-B!CSP is a combination of Event-B and CSP in which CSP controllers are used in conjunction with Event-B machines to allow a more explicit approach to control flow. Recent results have provided an approach to stepwise refinement of such combinations. This paper presents a simplified Bounded Retransmission Protocol case study, inspired by Abrial’s treatment of this example, to illustrate several aspects new in the approach. The case study includes refinement steps to illustrate four different aspects of this approach to refinement: (1) splitting events; (2) introducing convergent looping behaviour; (3) the relationship between anticipated, convergent, and devolved events; and (4) converging anticipated events.

Item Type: Other
Uncontrolled Keywords: Event-B, CSP, Bounded Retransmission Protocol, Stepwise Refinement
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Christina Daoutis
Date Deposited: 25 Mar 2011 13:58
Last Modified: 23 Sep 2013 18:40
URI: http://epubs.surrey.ac.uk/id/eprint/2766

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