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).
-
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:
- 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!
People
The people associated with the Lab are:
- Judy Bowen, Researcher (and recently completed PhD student);
- David Friggens, PhD student;
- Robi Malik,
Lecturer;
- Gian Perrone, former MSc student, now a PhD student in Denmark;
- Steve
Reeves,
Professor;
- David Streader, Senior Research Fellow;
- Mark
Utting, Associate Professor;
- Lindsay
Groves, Victoria University, Wellington;
- Martin
Henson University of Essex, U.K.;
- Bruno
Legeard,
Professor, University of Franche-Comté, France;
- Jing Sun,
University of Auckland.
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
|