Abstract
This paper develops a case study using the process algebra CSP to enable controlled interaction between B machines. This illustrates how B machines are essential components within a combined communicating system. The development steps used to build the case study are new: they are applications of theoretical results which allow us to focus on the external interface of a combined communicating system, compositionally verify it, and show that it is a refinement of a more abstract specification described in CSP. This allows safety and liveness properties to be established for combinations of communicating B machines.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial J. R.: The B Book: Assigning Programs to Meaning, CUP (1996).
Cavalcanti A., Sampaio A., and Woodcock J.: Refinement of Actions in Circus, In REFINE’02, FME Workshop, Copenhagen (2002).
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).
Formal Systems (Europe) Ltd.: Failures-Divergences Re.nement: FDR2 User Manual (1997), http://www.formal.demon.co.uk
Neilson D., Sorensen I. H.: The B-Technologies: a system for computer aided programming, B-Core (UK) Limited, Kings Piece, Harwell, Oxon, OX11 0PA (1999), http://www.b-core.com
Muntean T., Rolland O.:Distributed Refinement: application to the B Method, RCS’02, International Workshop on Re.nement of Critical Systems: Methods, Tools and Experience, Grenoble (2002)
Schneider S.: Concurrent and Real-time Systems: The CSP approach, Wiley (2000).
Schneider S.: The B-Method: An Introduction, Palgrave, 2001.
Schneider S., Treharne H.: Communicating B Machines. ZB2002, Grenoble, LNCS 2272, Springer, January (2002).
Schneider S., Treharne H.: CSP Theorems for Communicating B Machines. Technical Report CSD-TR-02-12, Dept. of Computer Science, Royal Holloway (2002).
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. ZB2000, York, LNCS 1878, Springer, September (2000).
Treharne H.: Controlling Software Specification. PhD Thesis, Royal Holloway, University of London (2000).
Treharne H., Schneider S.: Communicating B Machines (full version). Technical Report, RHUL (2001).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Treharne, H., Schneider, S., Bramble, M. (2003). Composing Specifications Using Communication. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_5
Download citation
DOI: https://doi.org/10.1007/3-540-44880-2_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40253-4
Online ISBN: 978-3-540-44880-8
eBook Packages: Springer Book Archive