Stopping computer calamities

A computing mix-up led to the loss of a NASA spacecraft in 1999 – but Strathclyde researchers are developing a technique which could help to prevent calamities like this in future.

How to prevent computer disasters

Computer science researchers at Strathclyde are developing software to help prevent programs carrying out – with potentially disastrous results - unintended tasks.

The software is aimed at guaranteeing that programs perform the computations they are designed to carry out. It'll be particularly useful for systems in areas where security is crucial and nothing can be left to chance, such as nuclear facilities, aeroplanes, and credit card transactions.

One particularly notorious example of a computing calamity is the case of NASA’s Mars Climate Orbiter spacecraft, which was lost in space in 1999 after one set of information used metric units while another used imperial units. However, the software being developed at Strathclyde has uses in all kinds of applications.

Co-investigator Professor Neil Ghani, of Strathclyde’s Department of Computer and Information Sciences, said:

Most software is tested by running it a certain times – and that’s good because it’s cheap and easy. However, it is not very certain – it might have failed on the next test had one more been run. To get more certainty, you need to use mathematical abstractions to prove conclusively that programs are correct. This is what our research is designed to provide – a specific technique to allow computers to check whether a program satisfies certain given properties, with 100% assurance.

Approach to research

Formal verification uses mathematical techniques to prove that programs actually perform the computations they are intended to perform – for example, that text editors do save a file when a ‘save’ command is issued, or that automatic pilots do correctly execute flight plans. It also ensures programs avoid performing unintended computations, such as leaking credit card details or launching nuclear weapons without authorisation.

Programmers make 15 to 50 errors per 1,000 lines of code and repairing these errors accounts for around 80% of project expenses. Programs are also continually increasing in size and becoming ever more sophisticated, meaning that formal verification is increasingly critical to modern software development.

The Strathclyde study aims to provide a simple, reusable and uniform framework for the development and use of logical relations, which is a key technology within program verification.

Collaborative research

The study also has input from experts with Microsoft and the Universities of Edinburgh and Copenhagen. It is funded by the Engineering and Physical Sciences Research Council.