Calamitous computer glitches, such as those that led to the loss of NASA’s £82 million Mars Climate Orbiter Spacecraft, could be prevented thanks to research by University of Strathclyde academics, says the university.
Dr Patricia Johann and Professor Neil Ghani, of Strathclyde’s Department of Computer and Information Sciences, aim to develop software that guarantees programs perform the computations they are designed to carry out.
Crucially, the software aims to stop programs performing unintended tasks, thus improving the reliability of safety-critical systems, such as those running nuclear facilities, aeroplanes and credit card transactions.
Professor Ghani, co-investigator on the £440,000 Engineering and Physical Sciences Research Council (EPSRC) funded project, said: “In an economy as relentlessly digital as the modern worldwide one - in which everything from toasters to interpersonal communications and global financial services are computerised - the need for formally-verified software cannot be overestimated."
Ghani said formal verification uses mathematical techniques to prove that programs actually perform the computations they are intended to perform, for example, that text editors really do save a file when a "save" command is issued, or that automatic pilots really do correctly execute flight plans.
Formal verification also ensures programs avoid performing unintended computations, such as leaking credit card details or launching nuclear weapons without authorisation.
Ghani said, “Since programmers make 15 to 50 errors per 1,000 lines of code, and since repairing them accounts for some 80 percent of project expenses, the ever-increasing size and sophistication of programs makes formal verification increasingly critical to modern software development.
“We aim to revolutionise a key technology within program verification, namely logical relations, by providing a framework for their development and use that is principled, conceptually simple, reusable and uniform, rather than ad hoc.”
The Mars Climate Orbiter Spacecraft was lost in September 1999 because one NASA team used imperial units while another used metric units for a key spacecraft operation. Ghani believes Strathclyde’s formal verification research could lead to similar errors being averted in the future.
He added that current testing procedures for software - which involve repeatedly running programs hundreds of times to detect errors - are "inadequate". Ghani said: “Most software is tested by running it a certain number of times, which is cheap and easy to do. However, it is not very certain as it might have failed on the next test had one more been run.”
He said that to get more certainty developers and testers needed to use mathematical abstractions to "prove conclusively" that programs are correct. The Strathclyde research will provide a specific technique to allow computers to check whether a program satisfies certain given properties, "with 100 per cent assurance".
Ghani believes there is a lucrative potential market for the research, which will also benefit from the input of experts from Microsoft and the Universities of Edinburgh and Copenhagen.
He said, “If we can make program verification cheaper, it will become a major selling point for safety-critical software, such as flight navigation systems. Once one company starts guaranteeing 100 percent accuracy in its products, others will immediately have to play catch-up.”