Advertisement

Communicating B Machines

  • Steve Schneider
  • Helen Treharne
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)

Abstract

This paper describes a way of using the process algebra CSP to enable controlled interaction between B machines. This approach supports compositional verification: each of the controlled machines, and the combination of controller processes, can be analysed and verified separately in such a way as to guarantee correctness of the combined communicating system. Reasoning about controlled machines separately is possible due to the introduction of guards and assertions into description of the controller processes in order to capture assumptions about other controlled machines and provide guarantees to the rest of the system. The verification process can be completely supported by difierent tools. The use of separate controller processes facilitates the iterative development and analysis of complex control flows within the system. The approach is motivated and illustrated with a non-trivial running example.

Keywords

B-Method CSP Combining Formalisms Concurrency 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrial J. R.: The B Book: Assigning Programs to Meaning, CUP (1996).Google Scholar
  2. 2.
    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).Google Scholar
  3. 3.
    Butler M. J.: A CSP Approach to Action Systems, D.Phil Thesis, Programming Research Group, Oxford University (1992).Google Scholar
  4. 4.
    Butler M. J.: An Approach to the Design of Distributed Systems with B AMN. In J. Bowen, M. Hinchey D. Till, editors, ZUM’97, Springer (1998), pp 223–241.Google Scholar
  5. 5.
    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).Google Scholar
  6. 6.
    Hoare C. A. R.: Communicating Sequential Processes, Prentice Hall (1985).Google Scholar
  7. 7.
    Jones C. B.: Specification and Design of (parallel) Programs. In R.E.A. Mason, editor, Information Processing’ 83. IFIP, North Holland (1983).Google Scholar
  8. 8.
    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).Google Scholar
  9. 9.
    Formal Systems (Europe) Ltd.: Failures-Divergences Refinement: FDR2 User Manual (1997), http://www.formal.demon.co.uk
  10. 10.
    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
  11. 11.
    Schneider S.: Concurrent and Real-time Systems: The CSP approach, Wiley (2000).Google Scholar
  12. 12.
    Schneider S.: The B-Method: An Introduction, Palgrave, 2001.Google Scholar
  13. 13.
    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).Google Scholar
  14. 14.
    Treharne H., Schneider S.: How to drive a B Machine. ZB2000, York, LNCS 1878, Springer, September (2000).Google Scholar
  15. 15.
    Treharne H.: Controlling Software Specifications. PhD Thesis, Royal Holloway, University of London (2000).Google Scholar
  16. 16.
    Treharne H., Schneider S.: Communicating B Machines (full version). Technical Report, RHUL (2001).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Steve Schneider
    • 1
  • Helen Treharne
    • 1
  1. 1.Department of Computer ScienceRoyal Holloway, University of LondonSurreyUK

Personalised recommendations