Department of Computer Science School of Computing and Mathematical Sciences

Formal Methods Laboratory

Software available

Tools for editing and translating μ-Charts

The CZT SourceForge website



The Formal Methods (FM) Laboratory was established during March 1999, and is now housed within and around the Software Engineering Lab at Waikato. We believe that the FM Lab is the first such in New Zealand, and it is the physical home to many in the FM Group.

The main job of the FM Lab is to be a base for the formal methods projects in the department. The funding for two of the original projects in the Lab finished some time ago, but for historical reasons we have kept the pages for those projects: the ISuRF project and the Z-lambda project . We most recently held a grant from FRST (a source of NZ government funding for science) which ran from 2002 to 2009. This funding was to carry on work in one main area, which can be seen as continuations fo the ISuRF and Z-lambda projects (which were also FRST-funded on two previous grants).

In all we held grants from FRST for 10 years, a record that we're very proud of.

We currently hold a FRST sub-contract which funds a Senior Fellowship (held by David Streader).

Return to Top

  • Modelling safety-critical systems

    We are working with Waikato DHB and also Gallaghers on various devices.

    We are also using, amongst other things, Esterel technology.

    Official Esterel Technologies Academic Partner Academic partner of Esterel Technologies, the provider of model-based solutions for DO-178B, EN 50128 and IEC 61508 safety-critical systems.

  • Putting together user-centred design (UCD) and formal methods: theories and tools

    This project is concerned with the development of methods for bringing together UCD and FM approaches (both of which are clearly needed) to system design and development.

    Information on this project is here.

    And look under the Departmental publications page here over the last few years to see the "Bowen and Reeves" papers which give lots of detaills of our method and its applications.

  • Components and Discrete Event Systems

    This work covers two areas: the components work is seeking to devleop theories and tools to allow us to specify and refine components, which can be thought of as things which have both public (interface) and private states and processes, and so has to bring together work from the state-based world (e.g. Z) and the process-based world (e.g. CSP). Simply "gluing the work together" does not, we believe, give the best outcome, so we are working on more subtle approaches to this problem.

    The work on discrete event systems (DES) seeks to extend the highly successful and practically-motivated languages and systems which exist in this area (and which are extensively used in industry) to allow such desirable features as modular development of systems. This work draws on techniques from the process algebra world.

  • Z-based refinement techniques: theory and application

    We intend to build on our existing theoretical work on developing logics and calculi for refinement of Z and Z-like specifications, and to consider the wider problem of incorporating formal methods into the general software engineering cycle. Specific goals are:

    • Further development of our theoretical framework to investigate fully the relationships between various kinds of refinement (particularly data refinement)
    • Further development of theory covering the use of standard Z within refinement
    • Developing techniques for supporting the use of refinement and other formal methods over the software-development life-cycle

  • Z support tools

    Here we will develop improved support tools for the Z specification language, to enable wider use of Z within NZ industry and worldwide. Good support tools are a necessary prerequisite for industry adoption, and the currently available Z tools are fragmented and do not work well together. There is a strong need to develop a more integrated framework which allows these tools to work together, and to complete some tools, such as animators, which are particularly needed for industry collaboration. Specific goals are:

  • Specification-Based Testing

    To reduce the cost of test design and improve the quality of software testing in the New Zealand software industry. This is being achieved by developing techniques and tools for the semi-automatic generation of test suites from Z specifications. The specific goal is:

    • Development of a translator from the Z specification language into the BZTT toolset

In 2004 we hosted "FM in NZ"---a formal methods day with speakers from around the world!


The people associated with the Lab are: 

All the people in New Zealand connected with the Formal Methods part of Software Engineering are in a group called the New Zealand Formal Program Development Colloquium (NZFPDC), which meets occasionally.

Please let us know if you want to be involved in any of our work, or would like more information.
See here for an enormous repository of information on all aspects of Formal Methods.

Return to Top

Web-administrator, Department of Computer Science, University of Waikato, Hamilton, New Zealand