Dr Patricia Johann and Prof 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.
This software aims to stop programs performing unintended tasks, thereby improving the reliability of safety-critical systems, such as those running nuclear facilities, aeroplanes, and credit card transactions.
Prof Ghani, co-investigator on the £440,000 EPSRC-funded project, said, ‘In an economy as relentlessly digital as the modern worldwide one – in which everything from toasters, to interpersonal communications, to global financial services are computerised – the need for formally-verified software cannot be overestimated.
‘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.
‘Since programmers make 15 to 50 errors per 1,000 lines of code – and since repairing them accounts for some 80 per cent 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.’
In September 1999 the Mars Climate Orbiter Spacecraft was lost because one NASA team used imperial units while another used metric units for a key spacecraft operation. Prof Ghani believes Strathclyde’s formal verification research could lead to similar errors being averted in the future.
He added in a statement that current testing procedures for software – which involve repeatedly running programs hundreds of times to detect errors – are inadequate.
Prof Ghani 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 per cent assurance.’
Professor Ghani believes there is a lucrative potential market for this 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 per cent accuracy in its products, others will immediately have to play catch-up.’
Report highlights significant impact of manufacturing on UK economy
I am not convinced that the High Value Manufacturing Centres do anything to improve the manufacturing processes - more to help produce products (using...