Critical advance for critical software systems
An animation program developed at the University of Queensland can quickly and cheaply check the accuracy of the mathematical design of computer software for critical systems such as air traffic control and blood bank stock monitoring.
Known as POSSUM, the program was developed in the University's Software Verification Research Centre.
Through use of a graphic interface, POSSUM provides a shortcut to the standard formal verification process required before software for critical systems is approved.
The process, although essential, is time consuming and costly, particularly if an error is eventually found in the mathematical design. After the mathematical specifications are completed, there is a long process of transformation and proof as it is refined into a language understood by computers.
POSSUM acts as though the computer language is already in place, interpreting, evaluating and testing the validity of mathematical code without going through the full refinement.
"It is a bit like a de-bugger, it's a good way to get rid of the bugs in the specifications, and much cheaper than formal proof," said Dan Hazel, a senior research officer at the University who began work on POSSUM in 1993 while a research student.
While not a replacement for formal verification methods, Mr Hazel says the pace of technological development will make the use of POSSUM for design assurance increasingly viable.
"More and more software is being trusted with critical systems responsibility, and sometimes it fails the test, such as in the Ariane 5 rocket explosion," he said.
"Because the price of computer capacity halves every year, it is difficult not to allow them to be in trusted positions, and the community is confronted with finding better ways of verifying the software."
POSSUM has already been used in a British Aerospace Australia missile decoy system known as NULKA, where formal design assurance was demanded by the Australian Defence Department's Safety Critical Systems Standard.
Other critical systems which could benefit from POSSUM include heart pacemakers, nuclear power stations, traffic monitoring and control, oil pipelines and production and police, fire and ambulance emergency response.
It will also be used as a teaching tool in Canada next year.
For further information, phone Mr Hazel on 336-51638, or contact him by e-mail at odin@csee.uq.edu.au
