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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial J. R.: The B Book: Assigning Programs to Meaning, CUP (1996).
Abrial J. R.:Extending B without Changing it (for Developing Distributed Systems). In H. Habrias, editor, Proc. of the 1st B Conference, Nantes, France (1996).
Butler M.J.: A CSP Approach to Action Systems. D.Phil Thesis, Programming Research group, Oxford University (1992).
Butler M.J.: csp2B: A Practical Approach to Combining CSP and B, In J.M. Wing, J. Woodcock, J. Davies, editors, FM’99 World Congress, Springer (1999).
Dijkstra E. W.: A Discipline of Programming, Prentice-Hall (1976).
Fischer C.: How to combine Z with a Process Algebra. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM’98 The Z formal Specification Notation, volume 1493 of LNCS, Springer (1998).
Fischer C.: CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS’97), volume 2, Chapman & Hall (1997).
Hoare C.A.R.: Communicating Sequential Processes, Prentice Hall (1985).
Morgan C.C.: Of wp and CSP. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries and J. Misra, editors, Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer (1990).
Roscoe A. W., Woodcock J. C. P. and Wulf L.: Non-interference through determinism. In D. Gollmann, editor, ESORICS 94, volume 875 of LNCS, Springer (1994).
Roscoe A. W.: The Theory and Practice of Concurrency, Prentice-Hall, 1997.
Scattergood J.B.: The Semantics of Machine-Readable CSP, Oxford University D.Phil thesis, 1998.
Schneider S.: Concurrent and Real-time Systems: The CSP approach, Wiley, 2000.
Stoy, J. E.: Denotational Semantics, MIT Press (1977).
Treharne H., Schneider S.: Using a Process Algebra to control B OPERATIONS. In K. Araki, A. Galloway and K. Taguchi, editors, IFM’99, York, Springer (1999).
Treharne H., Schneider S.: How to drive a B Machine (Full Version). Technical Report CSD-TR-00-03, Royal Holloway, University of London, May (2000).
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Treharne, H., Schneider, S. (2000). How to Drive a B Machine. In: ZB 2000: Formal Specification and Development in Z and B. ZB 2000. Lecture Notes in Computer Science, vol 1878. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44525-0_12
Download citation
DOI: https://doi.org/10.1007/3-540-44525-0_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67944-8
Online ISBN: 978-3-540-44525-8
eBook Packages: Springer Book Archive