Skip to main content
SpringerLink
Log in
Book cover

Refinement pp 121–147Cite as

State-Based Languages: Z and B

  • Chapter
  • First Online:

Abstract

This chapter defines refinement in Z, and shows how it derives from the relational model in Chap. 4. It discusses the similarities and differences with refinement in B. The approach taken in a state-based specification language is very different in emphasis from that in a process algebra. Process algebras stress the interaction between independent components (processes), so that communication and concurrency are key. State is implicit in such a description. A different approach is taken by a state-based language which, as the name suggests, considers the specification of state as the primary focus in a description. In this chapter we illustrate the approach to state-based specification by briefly introducing the Z and B notations, and showing how we can apply our theory of refinement to them.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   54.99
Price excludes VAT (USA)
  • Durable hardcover 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

Learn about institutional subscriptions

References

  1. Smith G (2000) The Object-Z specification language. Kluwer Academic Publishers, Boston

    Book  Google Scholar 

  2. Potter B, Sinclair J, Till D (1996) An introduction to formal specification and Z. International series in computer science, 2nd edn. Prentice Hall, New York (1991)

    Google Scholar 

  3. Ratcliff B (1994) Introducing specification using Z: a practical case study approach. McGraw-Hill, London

    Google Scholar 

  4. Bottaci L, Jones J (1995) Formal specification using Z: a modelling approach. International Thomson Publishing, London

    Google Scholar 

  5. Bowen JP (1996) Formal specification and documentation using Z: a case study approach. International Thomson Computer Press, London

    Google Scholar 

  6. Jacky J (1997) The way of Z: practical programming with formal methods. Cambridge University Press, Cambridge

    Google Scholar 

  7. Hayes IJ (ed) (1987) Specification case studies. International series in computer science, 2nd edn. Prentice Hall, New York (1993)

    Google Scholar 

  8. Spivey JM (1992) The Z notation: a reference manual. International series in computer science, 2nd edn. Prentice Hall, New York

    Google Scholar 

  9. ISO/IEC (2002) International standard 13568:2002 Information technology – Z formal specification notation – Syntax, type system and semantics

    Google Scholar 

  10. Spivey JM (1988) Understanding Z: a specification language and its formal semantics. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  11. Barden R, Stepney S, Cooper D (1994) Z in practice. BCS practitioner series, Prentice Hall, New York

    MATH  Google Scholar 

  12. Woodcock JCP, Davies J (1996) Using Z: specification, refinement, and proof. Prentice Hall, New York

    MATH  Google Scholar 

  13. Derrick J, Smith G (2004) Linear temporal logic and Z refinement. In: Rattray C, Maharaj S, Shankland C (eds) AMAST. Lecture notes in computer science, vol 3116. Springer, Berlin, pp 117–131

    Google Scholar 

  14. Derrick J, Smith G (2012) Temporal-logic property preservation under Z refinement. Form Asp Comput 24(3):393–416

    Article  MathSciNet  Google Scholar 

  15. Derrick J, Boiten EA (2014) Refinement in Z and Object-Z, 2nd edn. Springer, Berlin

    Book  Google Scholar 

  16. Derrick J, Wehrheim H Using coupled simulations in non-atomic refinement. In: Bert et al [39], pp 127–147

    Google Scholar 

  17. Derrick J, Wehrheim H Non-atomic refinement in Z and CSP. In: Treharne et al [40], pp 24–44

    Google Scholar 

  18. Boiten EA (2014) Introducing extra operations in refinement. Form Asp Comput 26(2):305–317

    Article  MathSciNet  Google Scholar 

  19. Derrick J, Boiten EA, Bowman H, Steen MWA Weak refinement in Z. In: Bert et al [39], pp 369–388

    Google Scholar 

  20. Derrick J, Boiten EA, Bowman H, Steen MWA (1998) Specifying and refining internal operations in Z. Form Asp Comput 10:125–159

    Article  Google Scholar 

  21. Derrick J, Wehrheim H (2007) On using data abstractions for model checking refinements. Acta Inf 44(1):41–71

    Article  MathSciNet  Google Scholar 

  22. Derrick J, North S, Simons T (2006) Issues in implementing a model checker for Z. In: Liu Z, He J (eds) ICFEM. Lecture notes in computer science, Springer, Berlin, pp 678–696

    Google Scholar 

  23. Smith G, Derrick J (2006) Verifying data refinements using a model checker. Form Asp Comput 18(3):264–287

    Article  Google Scholar 

  24. Smith G, Derrick J (2005) Model checking downward simulations. Electron Notes Theor Comput Sci 137(2):205–224

    Article  Google Scholar 

  25. Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York

    Book  Google Scholar 

  26. Schneider S (2001) The B-method: an introduction. Palgrave Macmillan, London

    Google Scholar 

  27. Wordsworth JB (1996) Software engineering with B. Addison-Wesley, Longman Publishing Co., Inc., Boston

    Google Scholar 

  28. Lano K (1996) The B language and method: a guide to practical formal development. FACIT series, Springer, Berlin

    Book  Google Scholar 

  29. Sekerinski E, Sere K (eds) (1999) Program development by refinement - case studies using the B method. FACIT, Springer, Berlin

    MATH  Google Scholar 

  30. Abrial J-R, Mussat L (1997) Specification and design of a transmission protocol by successive refinements using B. In: Broy M, Schieder B (eds) Mathematical methods in program development. NATO ASI series F: computer and systems sciences, vol 158. Springer, Berlin, pp 129–200

    Google Scholar 

  31. Nicholls JE (ed) (1990) Z user workshop, Oxford 1990. Workshops in computing, Springer, Berlin

    Google Scholar 

  32. Bowen JP, Nicholls JE (eds) (1992) Seventh annual Z user workshop. Springer, London

    Google Scholar 

  33. Bowen JP, Hall JA (eds) (1994) ZUM’94. Z user workshop. Workshops in computing, Springer, Cambridge

    Google Scholar 

  34. Bowen JP, Hinchey MG (eds) (1995) ZUM’95: The Z formal specification notation. Lecture notes in computer science, vol 967. Springer, Limerick

    Google Scholar 

  35. Bowen JP, Hinchey MG, Till D (eds) (1997) ZUM’97: The Z formal specification notation. Lecture notes in computer science, vol 1212. Springer, Berlin

    Google Scholar 

  36. Bowen JP, Fett A, Hinchey MG (eds) (1998) ZUM’98: The Z formal specification notation. Lecture notes in computer science, vol 1493. Springer, Berlin

    Google Scholar 

  37. Bowen JP, Dunne S, Galloway A, King S (eds) (2000) ZB2000: Formal specification and development in Z and B. Lecture notes in computer science, vol 1878. Springer, Berlin

    Google Scholar 

  38. Bert D, Bowen JP, Henson MC, Robinson K (eds) (2002) ZB 2002: formal specification and development in Z and B, 2nd international conference of B and Z users. Lecture notes in computer science, vol 2272. Springer, Berlin

    Google Scholar 

  39. Bert D, Bowen JP, King S, Waldén MA (eds) (2003) ZB 2003: formal specification and development in Z and B, third international conference of B and Z users. Lecture notes in computer science, vol 2651. Springer, Berlin

    Google Scholar 

  40. Treharne H, King S, Henson MC, Schneider SA (eds) (2005) ZB 2005: formal specification and development in Z and B, 4th international conference of B and Z users, Guildford, UK, 13–15 April 2005, proceedings. Lecture notes in computer science, vol 3455. Springer, Berlin

    Google Scholar 

  41. Börger E, Butler MJ, Bowen JP, Boca P (eds) (2008) ABZ 2008. Lecture notes in computer science, vol 5238. Springer, Berlin

    Google Scholar 

  42. Frappier M, Glässer U, Khurshid S, Laleau R, Reeves S (eds) (2010) ABZ 2010. Lecture notes in computer science, vol 5977. Springer, Berlin

    Google Scholar 

  43. Derrick J, Fitzgerald JA, Gnesi S, Khurshid S, Leuschel M, Reeves S, Riccobene E (eds) (2012) Abstract state machines, Alloy, B, VDM, and Z - third international conference, ABZ 2012. Lecture notes in computer science, vol 7316. Springer, Berlin

    Google Scholar 

  44. Smith G (1997) A semantic integration of Object-Z and CSP for the specification of concurrent systems. In: Fitzgerald J, Jones CB, Lucas P (eds) FME’97: industrial application and strengthened foundations of formal methods. Lecture notes in computer science, vol 1313. Springer, Berlin, pp 62–81

    Google Scholar 

  45. Smith G, Derrick J Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Hinchey and Liu [50], pp 293–302

    Google Scholar 

  46. Smith G, Derrick J (2001) Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Form Methods Syst Des 18:249–284

    Article  Google Scholar 

  47. Smith G, Derrick J, George C, Miao H (eds) (2002) Abstract specification in Object-Z and CSP. Formal methods and software engineering. Lecture notes in computer science, vol 2495. Springer, Berlin, pp 108–119

    Google Scholar 

  48. Derrick J, Smith G (2003) Structural refinement of systems specified in Object-Z and CSP. Form Asp Comput 15(1):1–27

    Article  Google Scholar 

  49. Butler M An approach to the design of distributed systems with B AMN. In: Bowen et al [35], pp 223–241

    Google Scholar 

  50. Hinchey MG, Liu S (eds) (1997) First international conference on formal engineering methods (ICFEM’97). IEEE Computer Society Press, Hiroshima, Japan

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Sheffield, Sheffield, UK

    John Derrick

  2. School of Computer Science and Informatics, De Montfort University, Leicester, Leicestershire, UK

    Eerke Boiten

Authors
  1. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eerke Boiten
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John Derrick .

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Derrick, J., Boiten, E. (2018). State-Based Languages: Z and B. In: Refinement. Springer, Cham. https://doi.org/10.1007/978-3-319-92711-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-92711-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-92709-1

  • Online ISBN: 978-3-319-92711-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation