How to Drive a B Machine.
Tools
Tools
Tools
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]](/style/images/fileicons/application_pdf.png) | PDF (deleted) Restricted to Repository staff only Available under License : See the attached licence file. 241Kb | |
![[img]](/style/images/fileicons/text_plain.png) | Plain Text (licence) 1516b | |
| PDF - Accepted Version Available under License : See the attached licence file. 237Kb |
Official URL: http://dx.doi.org/10.1007/3-540-44525-0_12
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) |
|---|---|
| Divisions: | Faculty of Engineering and Physical Sciences > Computing Science |
| Related URLs: | |
| ID Code: | 7215 |
| Deposited By: | Mr Adam Field |
| Deposited On: | 30 Sep 2011 15:26 |
| Last Modified: | 16 Feb 2013 16:10 |
Document Downloads
Repository Staff Only: item control page