Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2002: Integrated Formal Methods pp 165–184Cite as

Model Checking Object-Z Using ASM

  • Conference paper
  • First Online:

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

Abstract

A major problem with creating tools for Object-Z is that its high-level abstractions are difficult to deal with directly. Integrating Object-Z with a more concrete notation is a sound strategy. With this in mind, in this paper we introduce an approach to model-checking Object-Z specifications based on first integrating Object-Z with the Abstract State Machine (ASM) notation to get the notation OZ-ASM. We show that this notation can be readily translated into the specification language ASM-SL, a language that can be automatically translated into the language of the temporal logic model checker SMV.

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 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

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Del Castillo and K. Winter. Model checking support for the ASM high-level language. In S. Graf and M. Schwartzbach, editors, Proc. of 6th Int. Conference for Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2000), vol. 1785 of LNCS, Springer-Verlag, 2000.

    Chapter  Google Scholar 

  2. G. Del Castillo. The ASM Workbench. PhD thesis, Department of Mathematics and Computer Science of Paderborn University, Germany, 2000.

    Google Scholar 

  3. R. Duke and G. Rose. Formal Object-Oriented Specification Using Object-Z. Macmillan Press, 2000.

    Google Scholar 

  4. E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 996–1072. Elsevier Science Publishers, 1990.

    Google Scholar 

  5. C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway and K. Taguchi editors, Proceedings of the 1st International Conference on Integrated Formal Methods (IFM’99), pages 315–334. Springer-Verlag, 1999.

    Google Scholar 

  6. Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual, Oct 1997.

    Google Scholar 

  7. W. Grieskamp. A computation model for Z based on concurrent constraint resolution. In ZB2000-International Conference of Z and B Users, September, 2000.

    Google Scholar 

  8. Y. Gurevich. May 1997 Draft of the ASM Guide. Technical report, University of Michigan EECS Department, 1997.

    Google Scholar 

  9. Y. Gurevich. Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 2000.

    Google Scholar 

  10. G. Holzmann. Design and validation of protocols: A tutorial. In Computer Networks and ISDN Systems, volume XXV, pages 981–1017, 1993.

    Article  Google Scholar 

  11. G. Holzmann. The SPIN model checker. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.

    Google Scholar 

  12. D. Jackson. Nitpick: A checkable specification language. In Proc. of the First ACM SIGSOFT Workshop on Formal Methods in Software Practice, pages 60–69, 1996.

    Google Scholar 

  13. D. Jackson, I. Schechter and I. Shlyakhter. Alcoa: the Alloy constraint analyser. In Int. Conf. on Software Engineering, 2000.

    Google Scholar 

  14. J. Jacky and M. Patrick. Modelling, checking and implementing a control program for a radiation therapy machine. In R. Cleaveland, D. Jackson, editors, Proc. of the First ACM SIGPLAN Workshop on Automated Analysis of Software(AAS’97), pages 25–32, 1997.

    Google Scholar 

  15. G. Kassel and G. Smith. Model checking Object-Z classes: Some experiments with FDR. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001), IEEE Computer Society Press, 2001 (to appear).

    Google Scholar 

  16. K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  17. F. Corella, Z. Zhou, X. Song, M. Langevin and E. Cerny. Multiway Decision Graphs for automated hardware verification. In Formal Methods in System Design, 10(1), 1997.

    Google Scholar 

  18. A. Cimatti, E.M. Clarke, F. Giunchiglia and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, 11th Conference on Computer-Aided Verification (CAV’99), vol. 1633 of LNCS, Springer-Verlag, 1999.

    Chapter  Google Scholar 

  19. G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.

    Google Scholar 

  20. J.M. Spivey. The Z Notation-A Reference Manual. Prentice Hall, 1992.

    Google Scholar 

  21. S. Valentine. The programming language Z. Information and Software Technology, volume 37, number 5-6, pages 293–301, May-June, 1995.

    Article  Google Scholar 

  22. The VIS Group. VIS: A System for Verification and Synthesis. In R. Alur and T. Henzinger, editors, 8th Int. Conf. on Computer Aided Verifaction, (CAV’96). vol. 1102 of LNCS, Springer-Verlag, 1996.

    Google Scholar 

  23. K. Winter. Model Checking Abstract State Machines. PhD thesis, Technical University of Berlin, Germany, http://edocs.tu-berlin.de/diss/2001/winter_kirsten.htm, 2001.

    Google Scholar 

  24. K. Winter. Model checking with abstract types. In S. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier Science Publishers, 2001.

    Google Scholar 

  25. P. Zave. Formal description of telecommunication services in Promela and Z. In Calculational System Design, Proc. of the Nineteenth International NATO Summer School. IOS Press, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Verification Research Centre School of Information Technology and Electrical Engineering, University of Queensland, Australia

    Kirsten Winter & Roger Duke

Authors
  1. Kirsten Winter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roger Duke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electronics and Computer Science Declarative Systems and Software Engineering, University of Southampton, Highfield, Southampton, SO17 1BJ, UK

    Michael Butler

  2. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520, Turku, Finland

    Luigia Petre

  3. Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14, 20520, Turku, Finland

    Kaisa Sere

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Winter, K., Duke, R. (2002). Model Checking Object-Z Using ASM. In: Butler, M., Petre, L., Sere, K. (eds) Integrated Formal Methods. IFM 2002. Lecture Notes in Computer Science, vol 2335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47884-1_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-47884-1_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43703-1

  • Online ISBN: 978-3-540-47884-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation