Improving Software using Requirements Formalization - ISuRF 
  
 
 

• Introduction
• People
• Objectives
• Progress
• Publications
• Web-page of Waikato Formal Methods lab
• Web-page of Computer Science Department

This project is funded by the Government's New Economy Research Fund (NERF), administered by the Foundation for Research, Science and Technology (FRST). 

Introduction

Top of page

People

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

Tracey Yao , Victoria University, Wellington
 

Top of page

• Tools and problems for the New Zealand software industry

  Objective Statement:
  To identify and determine suitable tools and techniques to allow us to formalize the requirements for some typical problems from the New Zealand software industry.

  2000-2001

  • Develop and/or adapt tools and techniques that are needed to most effectively relate formal requirements to the software development techniques currently used by our industrial partners;
  • Report (via conference, journal and trade publications) on the tools that we propose to provide and what techniques will be appropriate for our industrial partners;
  • Via discussions and meetings with each industrial partner, decide on a set of requirements problems to be formalized.

• Case studies in formal requirements specification

  Objective Statement:
  To produce a set of examples of how industry currently solves the problem of requirements development and description, together with a matching set of examples which show how the same problems can be solved using formal techniques.

  2001-2002

  • Enhance the tools and techniques that are identified during the other objective to eliminate any major usability issues (after feedback from the users);
  • Develop formal requirements specifications for the problems isolated in the other objective, using tools and techniques as necessary and as they become available;
  • Report (via conference, journal and trade publications) on the problems industry gave us to work on, the tools and techniques we gathered or developed to attack the problems and how our new solutions compare with the original industrial ones.

Top of page

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.

The animation tools we have looked at so far are Possum, ZANS and ZAP. We have also used ZTC and Z/EVES to support our work using Z in the past, and probably will do in the future.

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

Top of page

Last updated on 18th January 2001