Combining CSP and B for Specification and Property Verification | SpringerLink
Skip to main content
Springer Nature Link
Log in

Combining CSP and B for Specification and Property Verification

  • Conference paper
FM 2005: Formal Methods (FM 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3582))

Included in the following conference series:

Abstract

ProB is a model checking tool for the B Method. In this paper we present an extension of ProB that supports checking of specifications written in a combination of CSP and B. We explain how the notations are combined semantically and give an overview of the implementation of the combination. We illustrate the benefit that appropriate use of CSP, in conjunction with our tool, gives to B developments both for specification and for verification purposes.

This research is being carried out as part of the EU funded research projects: IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems) and IST-2001-38059 ASAP (Advanced Specialization and Analysis for Pervasive Systems).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 83. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. U. B-Core (UK) Limited, Oxon. B-Toolkit, On-line manual, 1999. Available at, http://www.b-core.com/ONLINEDOC/Contents.html .

  4. Butler, M.J.: csp2B: A Practical Approach to Combining CSP and B. Formal Asp. Comput. 12(3), 182–198 (2000)

    Article  MATH  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  6. Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowmann, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), pp. 423–438. Chapman & Hall, Boca Raton (1997)

    Google Scholar 

  7. Formal Systems (Europe) Ltd. Failures-Divergence Refinement — FDR2 User Manual

    Google Scholar 

  8. Hartel, P., Butler, M., Currie, A., Henderson, P., Leuschel, M., Martin, A., Smith, A., Ultes-Nitsche, U., Walters, B.: Questions and answers about ten formal methods. In: Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, Trento, Italy (July 1999)

    Google Scholar 

  9. Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  10. Leuschel, M.: Design and implementation of the high-level specification language CSP(LP) in Prolog. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol. 1990, pp. 14–28. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  11. Leuschel, M., Butler, M.: ProB: A Model Checker for B.. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Leuschel, M., Turner, E.: Visualizing larger states spaces in ProB. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Mahony, B.P., Dong, S.: Blending Object-Z and Timed CSP: An introduction to TCOZ. In: 20th International Conference on Software Engineering (ICSE 1998), pp. 95–104 (1998)

    Google Scholar 

  14. Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Sci. Comput. Program. 40(1), 59–96 (2001)

    Article  MATH  Google Scholar 

  15. Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  16. Scattergood, J.B.: Tools for CSP and Timed-CSP. PhD thesis, Oxford University (1997)

    Google Scholar 

  17. Schneider, S., Treharne, H.: Verifying controlled components. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 87–107. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Smith, G.: A semantic integration of Object-Z and CSP for the specification of concurrent systems. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 62–81. Springer, Heidelberg (1997)

    Google Scholar 

  19. Steria, F.: Aix-en-Provence. Atelier B, User and Reference Manuals(1996), Available at, http://www.atelierb.societe.com/index_uk.html

  20. Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Electronics and Computer Science, University of Southampton, Highfield, Southampton, SO17 1BJ, UK

    Michael Butler & Michael Leuschel

  2. Institut für Informatik, Heinrich-Heine Universität Düsseldorf, Universitätsstr. 1, D-40225, Düsseldorf

    Michael Leuschel

Authors
  1. Michael Butler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, Newcastle University, NE1 7RU, Newcastle, UK

    John Fitzgerald

  2. School of Information Technology and Electrical Engineering, The University of Queensland, Australia

    Ian J. Hayes

  3. Institute of Computer Science, Polish Academy of Sciences,  

    Andrzej Tarlecki

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Butler, M., Leuschel, M. (2005). Combining CSP and B for Specification and Property Verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_16

Download citation

  • DOI: https://doi.org/10.1007/11526841_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27882-5

  • Online ISBN: 978-3-540-31714-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation