Improving Software using Requirements Formalization - ISuRF
This project is funded by the Government's New Economy Research Fund (NERF), administered by the Foundation for Research, Science and Technology (FRST).
Lindsay Groves, Victoria University, Wellington
Ray Nickson, Victoria University, Wellington
Steve Reeves, University of Waikato, Hamilton
Mark Utting, University of Waikato, Hamilton
Richard Mansfield, Victoria University, Wellington
, Victoria University, Wellington
Our most recent publications have been to do with work on specifying systems (especially reactive systems) using a chart-based language. We have given a uniform method for translating these charts to Z. This means thta we can prove things about the specified systems using tools like Z/EVES.
See the Publications page for papers on the charts.
Last year we produced our first report, which is a survey of the New Zealand software industry which looks at the ways it goes about gathering and writing down requirements and specifications. It has been published in the Waikato working papers series as number 99/8.
We have carried on working with our two partner companies. We are currently in the process of taking example software developments that they have be engaged on in the past and, purely from the requirements documents that they themselves used, we are working towards formal specifications written in Z (and perhaps other languages—this remains to be seen). We will then present these to the companies and see what comments they have. This will take us closer to our goal of seeing how such methods might be introduced into the NZ software industry in the future.
During the work mentioned in the previous paragraph, we have used (to date) three animation tools. The tools allow parts of a specification to be animated, in the sense that one can give input values to the specification and see what output values are given. Thus, they can be used as validation tools for the specification, i.e. to investigate the specification in order to see whether the specified system behaves as the requirements intend. The value of this is that we can see whether we have specified the correct system (as judged by the requirements before any coding has gone on. This technique is clearly going to save a lot of time and money if used more widely in the software industry.
Within the ISuRF project work has been done towards developing an animation tool for Z (called Jaza) and also an editor for the charts (AMuZed).
Web-administrator, Department of Computer Science, University of Waikato, Hamilton, New Zealand
Last updated on 18th January 2001