Waikato Formal Methods Group
Explore the work of the Waikato Formal Methods Group and their innovative approaches.
Since 1998, our Formal Methods lab has been at the forefront of computer science in New Zealand. We believe that programming is a core aspect of computer science and that rigorous mathematical modeling is essential for building reliable software.
Instead of relying on trial and error, which can be costly and time-consuming, we focus on developing languages and tools that allow us to precisely model and reason about systems before they're built. Our goal is to create software that consistently works as intended, free from errors and bugs.
One particular project is aimed at producing methods that will allow the development of user-interfaces to the same level of dependability as the functional part of a system. We are also developing tools for generating test suites from specifications, to improve the cost-effectiveness of testing. We are investigating languages and logics for dealing with refinement at a general level, and techniques for developing discrete event systems.
Driving the work of the lab are problems that we have been presented with by various parts of the New Zealand (and beyond) software development industry. This means that we can be sure our work is going to be useful for solving problems that are important to people outside the research environment.
Associate Dean Academic, Associate Professor
Professor
Projects
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.
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 can be found on Research Commons.
See the "Bowen and Reeves" papers which give lots of details of our method and its applications.
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.
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
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
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