Abstract
Community Z Tools (CZT) is an integrated framework for the Z formal specification language. In this paper, we show how it is also designed to support extensions of Z, in a way that minimises the work required to build a new Z extension. The goals of the framework are to maximise extensibility and reuse, and minimise code duplication and maintenance effort. To achieve these goals, CZT uses a variety of different reuse mechanisms, including generation of Java code from a hierarchy of XML schemas, XML templates for shared code, and several design patterns for maximising reuse of Java code. The CZT framework is being used to implement several integrated formal methods, which add object-orientation, real-time features and process algebra extensions to Z. The effort required to implement such extensions of Z has been dramatically reduced by using the CZT framework.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
ISO/IEC 13568: Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics. 1st edn. ISO/IEC (2002)
Malik, P., Utting, M.: CZT: A Framework for Z Tools. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 65–84. Springer, Heidelberg (2005)
Fischer, C.: How to combine Z with process algebras. Technical report, University of Oldenburg (1998)
Fischer, C.: Combination and Implementation of Process and Data: from CSP-OZ to Java. PhD thesis, University of Oldenburg (2000)
Woodcock, J., Cavalcanti, A.: A Concurrent Language for Refinement. In: 5th Irish Workshop on Formal Methods (2001)
Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)
Cavalcanti, A.L.C., Sampaio, A., Woodcock, J.C.P.: Unifying Classes and Processes. Journal on Software and Systems Modelling (2005) (to appear)
Mahony, B., Dong, J.S.: Timed Communicating Object-Z. IEEE Transactions on Software Engineering 26, 150–177 (2000)
Sherif, A., He, J.: Toward a Time Model for Circus. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613–624. Springer, Heidelberg (2002)
Tang, X., Woodcock, J.: Towards Mobile Processes in Unifying Theories. In: Cuellar, J., Liu, Z. (eds.) SEFM2004: the 2nd IEEE International Conference on Software Engineering and Formal Methods, pp. 44–53 (2004)
Schneider, S., Davies, J.: A Brief History of Timed CSP. Theoretical Computer Science 138, 243–271 (1995)
Roscoe, A.W.: The Theory and Practice of Concurrency, 1st edn. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1997)
Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994)
Hoare, C., Jifeng, H.: Unifying Theories of Programming. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)
Utting, M., Toyn, I., Sun, J., Martin, A., Dong, J.S., Daley, N., Currie, D.: ZML: XML Support for Standard Z. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 437–456. Springer, Heidelberg (2003)
Meisels, I., Saaltink, M.: Z/Eves 1.5 Reference Manual. ORA Canada, TR-97-5493-03d (1997)
Saaltink, M., Meisels, I.: The Core Z/Eves API (DRAFT). Technical Report TR-99-5540-xx, ORA Canada (2003)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, USA (1995)
Mai, Y., de Champlain, M.: A Pattern Language To Visitors. In: The 8th Annual Conference of Pattern Languages of Programs (PLoP 2001), Monticello, Illinois, USA (2001)
Martin, A.C.: Acyclic visitor. In: Martin, R.C., Riehle, D., Buschmann, F. (eds.) Pattern Languages of Program Design, vol. 3, Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1997)
Nordberg III, M.E.: Default and Extrinsic Visitor. In: Martin, R.C., Riehle, D., Buschmann, F. (eds.) Pattern Languages of Program Design, vol. 3, Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1997)
Barbosa, A.: A Parser for Circus. Graduation Research Project (2002)
Woodcock, J., Cavalcanti, A., Freitas, L.: Circus Operational Semantics. In: Proceedings of Formal Methods Europe (2005)
Xavier, M.: Circus Type-checker. Master’s thesis, Universidade Federal de Pernambuco, Brazil. In: preparation (2006)
Utting, M.: Data Structures for Z Testing Tools. Technical report, University of Waikato, Hamilton, New Zeland (1999)
Winikoff, M.: Analysing modes and subtypes in Z specifications. Technical Report 98/2, University of Melbourne, Department of Computer Science, Parkville, Victoria 3052, Australia (1998)
Cavalcanti, A.: A Refinement Calculus for Z. PhD thesis, Oxford University (1997), Also published as a PRG Technical Monograph at http://web.comlab.ox.ac.uk/oucl/publications/monos/prg-123.html
Freitas, L.: Model Checking Circus. PhD thesis, Univeristy of York (October 2005) (to appear)
Roscoe, A.W.: Model checking CSP. In: Book: A Classical Mind: Essays in Honour of C. A. R. Hoare, pp. 353–378 (1994)
Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing 5, 1–20 (1993)
Oliveira, M.: A Refinement Calculus for Circus. PhD thesis, University of York (December 2005) (to appear)
Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPowerZ. draft, Univeristy of York (2005)
Anderson, P., Goldsmith, M., Scattergood, B., Teitelbaum, T.: An Environment for Integrating Formal Methods Tools. In: User Interfaces for Theorem Provers (1997)
Martin, A.P., Gardiner, P.H.B., Woodcock, J.C.P.: A Tactic Calculus. Formal Aspects of Computing 8, 244–285 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, T., Freitas, L., Malik, P., Utting, M. (2005). CZT Support for Z Extensions. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_14
Download citation
DOI: https://doi.org/10.1007/11589976_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)