Skip to main content
SpringerLink
Log in

Proving Temporal Properties of Z Specifications Using Abstraction

  • Conference paper
  • First Online:
Book cover ZB 2003: Formal Specification and Development in Z and B (ZB 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2651))

Included in the following conference series:

Abstract

This paper presents a systematic approach to proving temporal properties of arbitrary Z specifications. The approach involves (i) transforming the Z specification to an abstract temporal structure (or state transition system), (ii) applying a model checker to the temporal structure, (iii) determining whether the temporal structure is too abstract based on the model checking result and (iv) refining the temporal structure where necessary. The approach is based on existing work from the model checking literature, adapting it to Z.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • 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.

References

  1. P. Cousot and R. Cousot. Systematic design of program analysis framework. In 6th ACM Symposium on Principles of Programming Languages, 1979.

    Google Scholar 

  2. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In A.P. Sistla E.A. Emerson, editor, Computer Aided Verification (CAV’00), volume 1855 of LNCS. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  3. E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, 1994.

    Article  Google Scholar 

  4. E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.

    Google Scholar 

  5. J. Derrick and E. Boiten. Refinement in Z and Object-Z, Foundations and Advanced Applications. Springer-Verlag, 2001.

    Google Scholar 

  6. P. Strooper D. Hazel and O. Traynor. Possum: An animator for the SUM specification language. In W. Wong and K. Leung, editors, Asia Pacific Software Engineering Conference (APSEC 97), pages 42–51. IEEE Computer Society, 1997.

    Google Scholar 

  7. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 996–1072. Elsevier Science Publishers, 1990.

    Google Scholar 

  8. S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Int. Conf. on Computer Aided Verification (CAV 97), volume 1254 of LNCS, pages 72–83. Springer-Verlag, 1997.

    Google Scholar 

  9. D. Jackson. Abstract model checking of infinite specifications. In M. Naftalin, T. Denvir, and M. Bertran, editors, Formal Methods Europe (FME’94), volume 873 of LNCS, pages 519–531. Springer-Verlag, 1994.

    Google Scholar 

  10. Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs 96), volume 1125 of LNCS, pages 283–298. Springer-Verlag, 1996.

    Google Scholar 

  11. C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.

    Google Scholar 

  12. A. Mota, P. Borba, and A. Sampaio. Mechanical abstraction of CSPZ processes. In L.-H. Eriksson and P. Lindsay, editors, Formal Methods Europe FME’2002), volume 2391 of LNCS, pages 163–183. Springer-Verlag, 2002.

    Google Scholar 

  13. M. Saaltink. The Z-Eves system. In J. Bowen, M. Hinchey, and D. Till, editors, International Conference of Z User (ZUM 97), volume 1212 of LNCS, pages 72–85. Springer-Verlag, 1997.

    Google Scholar 

  14. G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.

    Google Scholar 

  15. J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 2nd edition, 1992.

    Google Scholar 

  16. H. Saïdi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, Computer Aided Verification (CAV 99), volume 1633 of LNCS, pages 443–454. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  17. I. Toyn and J. McDermid. CADiZ: An architecture for Z tools and its implementation. Software — Practice and Experience, 25(3):305–330, 1995.

    Article  Google Scholar 

  18. H. Wehrheim. Data abstraction for CSP-OZ. In J. Woodcock and J. Wing, editors, World Congress on Formal Methods (FM’99), volume 1709 of LNCS. Springer-Verlag, 1999.

    Google Scholar 

  19. K. Winter and G. Smith. Compositional verification for Object-Z. In 3rd International Conference of Z and B Users (ZB 2003), LNCS. Springer-Verlag, 2003. This volume.

    Google Scholar 

  20. J. M. Wing and M. Vaziri-Farahani. A case study in model checking software systems. Science of Computer Programming, 28:273–299, 1997.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Verification Research Centre, University of Queensland, 4072, Australia

    Graeme Smith & Kirsten Winter

Authors
  1. Graeme Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kirsten Winter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire LSR-IMAG, CNRS, 681, rue de la Passerelle, BP 72, 38402, Saint-Martin-d’Heres Cedex, France

    Didier Bert

  2. CISM, London South Bank University, Borough Road, London, SE1 0AA, UK

    Jonathan P. Bowen

  3. Department of Computer Science, University of York, Heslington, York, YO10 5DD, UK

    Steve King

  4. Department of Computer Science, Åbo Akademi University, Lemminkäineng. 14 A, 20520, Turku, Finland

    Marina Waldén

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Smith, G., Winter, K. (2003). Proving Temporal Properties of Z Specifications Using Abstraction. 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_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-44880-2_17

  • 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

Publish with us

Policies and ethics

Search

Navigation