Advertisement

Checking Z Data Refinements Using an Animation Tool

  • Neil J. Robinson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)

Abstract

We describe how a Z animation tool can be used to check Z data refinements. We illustrate two approaches. In the first approach the tool is used to interactively step through operations of the abstract and concrete specifications, checking whether the refinement relationship holds. In the second approach the tool is used to automatically check refinements and to provide counter-examples should the refinement fail. We envisage these techniques being used in order to improve understanding of refinements and to help validate their correctness.

Keywords

Model Check IEEE Computer Society Concrete State Abstract Operation Test Oracle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J.-R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, Cambridge, UK, 1996.zbMATHGoogle Scholar
  2. 2.
    M. Butler, J. Grundy, T. Långbacka, R. Rukšėnas, and J. von Wright. The refinement calculator: Proof support for program refinement. In L. Groves and S. Reeves, editors, Formal Methods Pacific’ 97, pages 40–61. Springer-Verlag, 1997.Google Scholar
  3. 3.
    E. Clarke, O. Grumberg, and D. Long. Model-checking and abstraction. In Proc. of the 19th ACM Symposium on Principles of Programming Languages, pages 343–354. ACM Press, 1992.Google Scholar
  4. 4.
    P. H. B. Gardiner and C. Morgan. A single complete rule for data refinement. Formal Aspects of Computing, 5:367–382, 1993.zbMATHCrossRefGoogle Scholar
  5. 5.
    N. Hamilton, D. Hazel, P. Kearney, O. Traynor, and L. Wildman. A complete formal development using Cogito. In C. McDonald, editor, Computer Science’ 98: Proc. 21st Australasian Computer Science Conference, pages 319–330. Springer-Verlag, 1998.Google Scholar
  6. 6.
    I. J. Hayes. Correctness of data representations. In Proceedings of the 2nd Australian Software Engineering Conference (ASWEC-87), Canberra, pages 75–86. IREE (Australia), May 1987.Google Scholar
  7. 7.
    D. Hazel, P. Strooper, and O. Traynor. Possum: An animator for the Sum specification language. In W. Wong and K. Leung, editors, Proceedings Asia-Pacific Software Engineering Conference and International Computer Science Conference, pages 42–51. IEEE Computer Society Press, December 1997.Google Scholar
  8. 8.
    C. A. R. Hoare and Jifeng He. Unified Theories of Programming. Prentice Hall International Series in Computer Science, 1998.Google Scholar
  9. 9.
    C. A. R. Hoare, Jifeng He, and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2):71–76, May 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    D. Jackson and C. A. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering, 22(7):484–495, July 1996.CrossRefGoogle Scholar
  11. 11.
    W. Johnston and L. Wildman. The Sum reference manual. Technical Report 99-21, Software Verification Research Centre, School of Information Technology, The University of Queensland, Brisbane 4072, Australia, November 1999.Google Scholar
  12. 12.
    D. T. Jordan, C. J. Locke, J. A. McDermid, C. E. Parker, B. A. P. Sharp, and I. Toyn. Literate formal development of Ada from Z for safety critical applications. In Proceedings of SafeComp’94. ISA, 1994.Google Scholar
  13. 13.
    J. McDonald and P. Strooper. Translating Object-Z specifications to passive test oracles. In John Staples, Michael Hinchey, and Shaoying Liu, editors, Second International Conference on Formal Engineering Methods, Brisbane, Australia, December 9-11, 1998, pages 165–174, 1998.Google Scholar
  14. 14.
    T. Miller and P. Strooper. Animation can show only the presence of errors, never their absence. In D. D. Grant and L. Sterling, editors, Proceedings of the Australian Software Engineering Conference, ASWEC 2001, Canberra, Australia, pages 76–85. IEEE Computer Society Press, 2001.Google Scholar
  15. 15.
    T. Miller and P. Strooper. Combining the animation and testing of abstract data types. In Proceedings of the Second Asia-Pacific Conference on Quality Software, APAQS 2001, Hong Kong. IEEE Computer Society Press, December 2001. (to appear).Google Scholar
  16. 16.
    N. J. Robinson and C. Fidge. Visualisation of refinements. In D. D. Grant and L. Sterling, editors, Proceedings of the Australian Software Engineering Conference, ASWEC 2001, Canberra, Australia, pages 244–251. IEEE Computer Society Press, 2001.Google Scholar
  17. 17.
    S. Stepney, D. Cooper, and J. Woodcock. More powerful Z data refinement: Pushing the state of the art in industrial refinement. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM’98: The Z Formal Specification Notation, 11th International Conference of Z Users, Lecture Notes in Computer Science, pages 284–307. Springer-Verlag, 1998.Google Scholar
  18. 18.
    H. Waeselynck and S. Behnia. B model animation for external verification. In J. Staples, M. Hinchey, and S. Liu, editors, Second International Conference on Formal Engineering Methods, Brisbane, Australia, December 9-11, 1998, pages 36–45. IEEE Computer Society Press, 1998.Google Scholar
  19. 19.
    J. Woodcock and J. Davies. Using Z: Specification, refinement, and proof. International Series in Computer Science. Prentice Hall, 1996.Google Scholar

Copyright information

© Springer-VerlagBerlin Heidelberg 2002

Authors and Affiliations

  • Neil J. Robinson
    • 1
  1. 1.Software Verification Research CentreThe University of QueenslandBrisbaneAustralia

Personalised recommendations