Model Checking is a widely adopted technique for detecting and diagnosing design errors in computer hardware and software systems. At the heart of the method stands an algorithm which systematically considers various possible states of a given hardware or software design, reporting of any inconsistencies found between the known program specifications and the actual system configurations. These “logical errors” are a common problem in different areas of computing, such as digital circuit design, software, and networking systems.
|
E. Clarke, currently a Professor at Carnegie Mellon University and E. Emerson from the University of Texas, in Austin, initially researched the idea of Model Checking at Harvard University in 1981. Independently from their research and approximately at the same time, J. Sifakis and his colleague J. P. Queille of the University of Grenoble in France worked on the development of a theoretical technique of the Model Checking method. Based on this theoretical model, the scientists derived a fully automated approach, which today is one of the mostly used verification methods in both hardware and software design.
|
Since its introduction, Model Checking has proven to be highly effective in the industry, used for such purposes as improving the reliability and security of complex computer chips, software device drivers, and networking protocols. One of the major benefits of the system is that it not only reports a problem, but also provides designers with detailed information regarding the source of the inconsistency by identifying the encountered “logical” counterexample, helping them in the “debugging” process.
|
The president of ACM, Stuart Feldman, said the method had a major impact especially on the semiconductor industry. “These industries face a technology of explosion in which products of unprecedented complexity have to operate as expected for companies to survive. This verification advance enabled these industries to shorten time to market and increase product integrity. Without the conceptual breakthrough pioneered by these researchers we might still be stuck with chips that have many errors and would lack the speed of today’s equipment. This is a great example of an industry-transforming technology arising from highly theoretical research” – he said.
TFOT reported on the 2006 Turing Award, which was granted to Frances Allen from IBM.
More information on this year’s recipients of the Turing Award can be found on the ACM official website.
