Advertisement

The Object-Z Specification Language

  • V. S. Alagar
  • K. Periyasamy
Part of the Texts in Computer Science book series (TCS)

Abstract

The Z notation is more popular and is easy to use, but it is procedural in nature. A Z specification starts with a global state definition. Operations are then specified to manipulate the state variables. The procedural nature of Z specification makes the specifiers to think in terms of one global state space, and operations and functions to act on that global state. Practitioners of the object-oriented approach attempted to use the Z notation in an object-oriented style (Stepney et al. in Object orientation in Z, Springer, Berlin, 1992). They tried to model each object as a separate Z specification and thereby made each object as an independent and reusable entity. Composition of objects and interactions among objects were specified using schema calculus. However, this effort was not fruitful because the intrinsic properties of object-orientation such as encapsulation, inheritance and polymorphism were not captured by the Z specification written in object-oriented style. In order to utilize the full expressive power of the object-oriented approach, several object-oriented extensions of the Z notations were developed. MooZ (Cornelio and Borba in Software reuse: advances in software reusability, vol. 1844 of Lecture notes in computer science, Springer, Berlin, pp. 47–102, 2000; Cordeiro et al. in FME’94: industrial benefits of formal methods, vol. 873 of Lecture notes in computer science, Springer, Berlin, pp. 306–325, 1994), ZEST (Stepney et al. (eds) in Object orientation in Z, Springer, Berlin, 1992), Z++ (Stepney et al. (eds) in Object orientation in Z, Springer, Berlin, 1992) and Object-Z (Duke and Rose in Formal object-oriented specification using Object-Z, MacMillan, New York, 2000; Smith in The Object-Z specification language, Kluwer Academic, Norwell, 2000) are some of them. Among these extensions, Object-Z became more popular because of its literature support and tool support.

Keywords

Composition Operator Network Manager Sequential Composition Class Account Predicate Part 
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.

References

  1. 1.
    Alagar VS, Periyasamy K (1996) Real-time Object-Z: a language for the specification and design of real-time reactive system. Technical report, Department of Computer Science, Concordia University Google Scholar
  2. 2.
    Amálio N, Polack F (2003) Comparison of formalisation approaches of UML class constructs in Z and Object-Z. In: International conference of Z and B users (ZB 2003). Lecture notes in computer science, vol 2561. Springer, Berlin Google Scholar
  3. 3.
    Carrington D, MacColl I, McDonald J, Murray L, Strooper P (2000) From Object-Z specifications to ClassBench test suites. Softw Test Verif Reliab 10(2):111–137 CrossRefGoogle Scholar
  4. 4.
    Cornelio M, Borba P (2000) Structuring mechanisms for an object-oriented formal specification language. In: Software reuse: advances in software reusability. Lecture notes in computer science series, vol 1844. Springer, Berlin, pp 47–102 Google Scholar
  5. 5.
    Cordeiro VAO, Sampaio A, Meira SL (1994) From MooZ to Eiffel—a rigorous approach to system development. In: FME’94: industrial benefits of formal methods. Lecture notes in computer science, vol 873, pp 306–325 CrossRefGoogle Scholar
  6. 6.
    Derrick J (2003) Timed CSP and Object-Z. In: International conference of Z and B users (ZB 2003). Lecture notes in computer science, vol 2561. Springer, Berlin Google Scholar
  7. 7.
    Derrick J, Boiten E (2001) Refinement in Z and Object-Z, foundations and advanced applications. Springer, Berlin MATHGoogle Scholar
  8. 8.
    Derrick J, Smith G (2003) Structural refinement of systems specified in Object-Z and CSP. Formal Aspects Comput 15(1):1–27 MATHCrossRefGoogle Scholar
  9. 9.
    Dong JS, Li YF, Sun J, Sun J, Wong H (2002) XML-based static type checking and dynamic visualisation for TCOZ. In: International conference on formal engineering methods (ICFEM 2002). Lecture notes in computer science, vol 2495. Springer, Berlin Google Scholar
  10. 10.
    Duke R, Rose G (2000) Formal object-oriented specification using Object-Z. MacMillan, New York Google Scholar
  11. 11.
    Fukagawa M, Hikita T, Yamazaki H (1994) A mapping system from Object-Z to C++. In: 1st Asia-Pacific software engineering conference (APSEC94). IEEE Computer Society, Los Alamitos Google Scholar
  12. 12.
    Griffiths A (1995) From Object-Z to Eiffel: a rigorous development method. In: Technology of object-oriented languages and systems: TOOLS 18. Prentice Hall, New York Google Scholar
  13. 13.
    Griffiths A (1996) An extended semantic foundation for Object-Z. In: Asia-Pacific software engineering conference (APSEC’96). IEEE Computer Society, Los Alamitos Google Scholar
  14. 14.
    Griffiths A (1997) A semantics for recursive operations in Object-Z. In: Formal methods Pacific (FMP’97). Springer, Berlin Google Scholar
  15. 15.
    Gruer P, Hilaire V, Koukam A (2004) Heterogeneous formal specification based on Object-Z and state charts: semantics and verification. J Syst Softw 70(1–2):95–105 CrossRefGoogle Scholar
  16. 16.
    Hilaire V, Simonin O, Koukam A, Ferber J (2004) A formal approach to design and reuse agent and multiagent models. In: Agent oriented software engineering (AOSE 04). Lecture notes in computer science Google Scholar
  17. 17.
    Hussey A (1999) Formal object-oriented user-interface design. Technical report 99-09, Software Verification Research Center, University of Queensland, Australia Google Scholar
  18. 18.
    Hussey A, Carrington D (1998) An empirical study of formal user-interface design. HCI Lett 1(1):19–24 Google Scholar
  19. 19.
    Johnston W (1996) A type checker for Object-Z. SVRC technical report No 96–24 Google Scholar
  20. 20.
    Kassel G, Smith G (2001) Model checking Object-Z classes: some experiments with FDR. In: Asia-Pacific software engineering conference (APSEC). IEEE Press, New York Google Scholar
  21. 21.
    Kim S-K, Carrington D (2002) A formal metamodeling approach to transformation between the UML state machine and Object-Z. In: International conference on formal engineering methods (ICFEM 2002). Lecture notes in computer science, vol 2495. Springer, Berlin Google Scholar
  22. 22.
    Lano K, Haughton H (eds) (1994) Object oriented specification case studies. Prentice Hall, New York MATHGoogle Scholar
  23. 23.
    Mahony B, Dong JS (2000) Timed communicating Object Z. IEEE Trans Softw Eng 26(2):150–177 CrossRefGoogle Scholar
  24. 24.
    Malik P, Utting M (2005) CZT: a framework for Z tools. In: Lecture notes in computer science, vol 3455, pp 65–84 Google Scholar
  25. 25.
    McComb T, Smith G (2003) Animation of Object-Z specifications using a Z animator. In: International conference on software engineering and formal methods (SEFM). IEEE Computer Society, Los Alamitos Google Scholar
  26. 26.
    Miao H, Lui L, Li L (2002) Formalizing UML models with Object-Z. In: International conference on formal engineering methods (ICFEM 2002). Lecture notes in computer science, vol 2495. Springer, Berlin Google Scholar
  27. 27.
    Moreira A, Arau’jo J (2000) Generating Object Z specifications from use cases. In: Filipe J (ed) Enterprise information systems. Kluwer Academic, Norwell, pp 43–51. ISBN 0-7923-6239-X Google Scholar
  28. 28.
    Moller M, Olderog E-R, Rasch H, Wehrheim H (2004) Linking CSP-OZ with UML and Java: a case study. In: International conference on integrated formal methods (IFM 2004). Lecture notes in computer science, vol 2999. Springer, Berlin Google Scholar
  29. 29.
    Parker T (2008) TOZE: a graphical editor and type checker for Object-Z. Masters thesis, Department of Computer Science, University of Wisconsin-La Crosse Google Scholar
  30. 30.
    Periyasamy K, Alagar VS, Subramanian S (1998) Deriving test cases from Object-Z specifications. In: TOOLS USA’98 (technology of object-oriented languages and systems). IEEE Computer Society, Los Alamitos Google Scholar
  31. 31.
    Periyasamy K, Alagar VS (1998) Extending Obejct-Z for specifying real-time systems. In: TOOLS USA’97: technology of object-oriented languages and systems. IEEE Computer Society, Los Alamitos Google Scholar
  32. 32.
    Qin SC, Dong JS, Chin WN (2003) A semantic foundation of TCOZ in unifying theory of programming. In: International FME symposium (FM’03). Lecture notes in computer science. Springer, Berlin Google Scholar
  33. 33.
    Roe D, Broda K, Russo A (2003) Mapping UML models incorporating OCL constraints into Object-Z. Technical report 2003/9, Imperial College, London Google Scholar
  34. 34.
    Smith G (1992) An object-oriented approach to formal specification. PhD thesis, University of Queensland Google Scholar
  35. 35.
    Smith G (1995) A fully abstract semantics of classes for Object-Z. Formal Aspects Comput 7(3):289–313 CrossRefGoogle Scholar
  36. 36.
    Smith G (1995) Reasoning about Object-Z specifications. In: Asia-Pacific software engineering conference (APSEC ’95). IEEE Computer Society, Los Alamitos Google Scholar
  37. 37.
    Smith G (1995) Formal verification of Object-Z specifications. SVRC Technical report 95-55 Google Scholar
  38. 38.
    Smith G (2000) The Object-Z specification language. Kluwer Academic, Norwell MATHCrossRefGoogle Scholar
  39. 39.
    Smith G (2000) Recursive schema definitions in Object-Z. In: ZB2000: international conference of B and Z users. Lecture notes in computer science, vol 1878. Springer, Berlin Google Scholar
  40. 40.
    Smith G (2002) An integration of real-time Object-Z and CSP for specifying concurrent real-time systems. In: International conference on integrated formal methods (IFM 2002). Lecture notes in computer science, vol 2335. Springer, Berlin Google Scholar
  41. 41.
    Smith G (2004) A formal framework for modelling and analysing mobile systems. In: Australasian computer science conference (ACSC). Australian Computer Society, Sydney Google Scholar
  42. 42.
    Smith G, Derrick J (2001) Specification, refinement and verification of concurrent systems—an integration of Object-Z and CSP. Form Methods Syst Des 18(3):249–284 MATHCrossRefGoogle Scholar
  43. 43.
    Smith G, Derrick J (2002) Abstract specification in Object-Z and CSP. In: International conference on formal engineering methods (ICFEM 2002). Lecture notes in computer science, vol 2495. Springer, Berlin Google Scholar
  44. 44.
    Smith G, Duke R (1992) Specifying concurrent systems using Object-Z. In: 15th Australian computer science conference (ACSC-15) Google Scholar
  45. 45.
    Smith G, Hayes I (2002) An introduction to real-time Object-Z. Form Aspects Comput 13(2):128–141 MATHCrossRefGoogle Scholar
  46. 46.
    Stepney S, Barden R, Cooper D (eds) (1992) In: Object orientation in Z. Springer, Berlin Google Scholar
  47. 47.
    Sun J, Dong JS, Liu J, Wang H (2001) An XML/XSL approach to visualize and animate TCOZ. In: 8th Asia-Pacific software engineering conference (APSEC’01). IEEE Press, New York Google Scholar
  48. 48.
    Taylor C, Derrick J, Boiten E (2000) A case study in partial specification: consistency and refinement for Object-Z. In: International conference on formal engineering methods (ICFEM). IEEE Computer Society, Los Alamitos Google Scholar
  49. 49.
    Taguchi K, Dong JS (2002) An overview of mobile Object-Z. In: International conference on formal engineering methods (ICFEM 2002). Lecture notes in computer science, vol 2495. Springer, Berlin Google Scholar
  50. 50.
    Taguchi K, Dong JS, Ciobanu G (2004) Relating Pi-calculus to Object-Z. In: IEEE international conference on engineering complex computer systems (ICECCS’04). IEEE Press, New York Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations