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] PDF (deleted)
fulltext.pdf
Restricted to Repository staff only
Available under License : See the attached licence file.

Download (241Kb)
[img] Plain Text (licence)
licence.txt

Download (1516b)
[img]
Preview
PDF
zb2000.pdf - Accepted Version
Available under License : See the attached licence file.

Download (237Kb)

Abstract

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)
Related URLs:
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Mr Adam Field
Date Deposited: 30 Sep 2011 14:26
Last Modified: 23 Sep 2013 18:45
URI: http://epubs.surrey.ac.uk/id/eprint/7215

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