University of Surrey

Test tubes in the lab Research in the ATI Dance Research

How to Drive a B Machine.

Treharne, H and Schneider, S (2000) How to Drive a B Machine. In: ZB 2000: Formal Specification and Development in Z and B, First International Conference of B and Z Users, 2000-08-29 - 2000-09-02, York, UK.

[img] Text (deleted)
Restricted to Repository staff only
Available under License : See the attached licence file.

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

Download (1kB)
zb2000.pdf - Accepted version Manuscript
Available under License : See the attached licence file.

Download (243kB)


The B-Method is a state-based formal method that describes behaviour in terms of MACHINES whose states change under OPERATIONS. The process algebra CSP is an event-based formalism that enables descriptions of patterns of system behaviour. We present a combination of the two views where a CSP process acts as a control executive and its events simply drive corresponding OPERATIONS. We define consistency between the two views in terms of existing semantic models. We identify proof conditions which are strong enough to ensure consistency and thus guarantee safety and liveness properties.

Item Type: Conference or Workshop Item (UNSPECIFIED)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Treharne, H
Schneider, S
Date : 2000
DOI : 10.1007/3-540-44525-0_12
Contributors :
ContributionNameEmailORCID, JP, S, A, S,
Related URLs :
Depositing User : Mr Adam Field
Date Deposited : 30 Sep 2011 14:26
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