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.
|PDF - Accepted Version |
Available under License : See the attached licence file.
|Plain Text (licence)|
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|
|Deposited By:||Symplectic Elements|
|Deposited On:||29 Sep 2011 12:36|
|Last Modified:||16 Feb 2013 16:11|
Repository Staff Only: item control page