Formal Methods Laboratory

Software available

Tools for editing and translating μ-Charts

The CZT SourceForge website

• Introduction
• Projects
• People
• Publications--look here under the names of FM people for our publications

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

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

  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:

  • To get the animation tool integrated with other Z tools in the CZT project
  • To extend to graphical animation display of Z specifications

• 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