The AM Turing Award for information technology innovation has been awarded to a group of academics researching ways to reduce errors in complex hardware and software systems.
Edmund M Clarke, of Carnegie Mellon University, E Allen Emerson, of the University of Texas at Austin, and Joseph Sifakis, of the University of Grenoble, were awarded the $250,000 (£127,000) prize by IT professional organisation the Association for Computing Machinery (ACM) in New York for their development of "model checking" verification technology.
ACM claims the researchers' work has transformed model checking from a theoretical technique into a fully automated process that enables both hardware and software engineers to find errors in complex system designs.
ACM president Stuart Feldman said the work of Clarke, Emerson and Sifakis has had a major impact on designers and manufacturers of semiconductor chips. "These industries face a technology explosion in which products of unprecedented complexity have to operate as expected for companies to survive. Without the conceptual breakthrough pioneered by these researchers, we might still be stuck with chips that have many errors and would lack the power and speed of today's equipment," he said.
Model checking as a standard procedure for quality assurance has helped IT engineers gain mathematically measured confidence that complex computer systems and software applications meet their intended specifications. The procedure is also commonly used in the verification of designs for integrated circuits such as microprocessors, as well as communication protocols, software device drivers, real-time embedded systems and security algorithms.
Logical errors in digital circuit designs, software architecture or communication protocols can present a potentially big problem for system designers. They can result in delays in getting new products to market, failure of critical systems already in use, and expensive replacement of faulty hardware and patching of flawed software.
Read this
Photos: Bringing Colossus back to life
Bletchley Park's rebuilt WWII Colossus codebreaker has recently been kicked back into action after a 14-year rebuild project...
"You simply can't do enough testing, so any methodology that improves the quality of computer systems will raise confidence in their use whether they are deployed in mission-critical environments or otherwise. These challenges will be even greater in the future, as more and more systems are integrated and given global reach. But these advancements should inspire all systems developers to strive to eliminate errors before they make their way into the technical design process," said Vinod Bhatia, operations director for UK-headquartered modelling specialists Paragon Simulation.
Model checking began life as an academic research concept nearly three decades ago. The continuing research of Clarke, Emerson, Sifakis and others has led to the creation of new logics, as well as new algorithms and theoretical results, it is claimed.
First awarded in 1966, the AM Turing Award was named after Alan M Turing, the British mathematician who articulated the mathematical foundation and limits of computing and who was a key contributor to the Allied cryptanalysis of the German Enigma cipher during World War II.
