Strathclyde University makes planes, nuclear reactors and spacecraft bug free
Calamitous computer glitches, such as those that led to the loss of NASAs 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 Strathclydes 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 Strathclydes 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.
See original here:
Strathclyde University makes planes, nuclear reactors and spacecraft bug free