University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Augmenting B with control annotations

Ifill, W, Schneider, S and Treharne, H (2007) Augmenting B with control annotations In: 7th International Conference of B Users, 2007-01-17 - 2007-01-19, Univ Franche Comte, Besancon, FRANCE.

b07.pdf - Accepted version Manuscript
Available under License : See the attached licence file.

Download (139kB)
[img] Text (licence)

Download (1kB)


CSP||B is an integration of the process algebra Communicating Sequential Processes (CSP), and the B-Method, which enables consistent controllers to be written for B machines in a verifiable way. Controllers are consistent if they call operations only when they are enabled. Previous work has established a way of verifying consistency between controllers and machines by translating control flow to AMN and showing that a control loop invariant is preserved. This paper offers an alternative approach, which allows fragments of control flow expressed as annotations to be associated with machine operations. This enables designers’ understanding about local relationships between successive operations to be captured at the point the operations are written, and used later when the controller is developed. Annotations provide a bridge between controllers and machines, expressing the relevant aspects of control flow so that controllers can be verified simply by reference to the annotations without the need to consider the details of the machine operations. This paper presents the approach through two instances of annotations with their associated control languages, covering recursion, prefixing, choice, and interrupt.

Item Type: Conference or Workshop Item (UNSPECIFIED)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Ifill, W
Schneider, S
Treharne, H
Date : 2007
DOI : 10.1007/11955757_6
Contributors :
ContributionNameEmailORCID, J, O BERLIN,
Depositing User : Symplectic Elements
Date Deposited : 29 Sep 2011 11:36
Last Modified : 31 Oct 2017 14:09

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