These days hardware and software systems are progressively being used in safety-critical domains, such as automated transportation networks and electronic military and medicine equipment. This makes the accuracy of their analysis of vital importance since an uncaught system bug can endanger human life or lead to a significant financial loss.
Traditionally, the analysis of these systems has been accomplished using paper-and-pencil methods, or computer simulations. However, these techniques do not ascertain 100 percent correctness and, thus, may lead to unfortunate incidents caused by erroneous systems deployed in safety-critical domains.
Some examples of such incidents include the death of three people between 1985 and 1987 due to a software bug in the cancer therapy machine Therac-25; a net loss of around $500 million to Intel in 1994 from a hardware error in the floating -point-division unit of its Pentium 4 processor; the crash of the US $370 million spacecraft “Mars Polar Lander” in 1999 due to spurious signals that gave a false indication about the aircraft’s landing; and, the loss of 228 human lives in the Air France crash in 2009 caused by inaccurate measurement of airspeed.
To make system analysis more reliable, a technique is needed that can combine the precision of paper-and-pencil based mathematical methods and the rigor of book-keeping using computers. Such a technique can be used to handle complex systems without worrying about the possibility of human error. Formal verification methods, which are primarily based on theoretical computer science fundamentals like logic calculi, automata theory, and strongly type systems, fulfill these requirements.
Formal analysis of a system involves construction of a computer-based mathematical model of the given system and verification that this model meets rigorous specifications of the intended behavior. Due to the mathematical nature of the analysis, 100 percent accuracy can be guaranteed.
The use of formal verification methods dates back to the 1970s when computer-aided design (CAD) tools were developed for software verification. However, interest in application of formal methods for software verification soon diminished since software bugs could be easily fixed by releasing a software patch. The added reliability of software was not worth the rigorous exercise of formal verification.
There was some research activity related to formal verification of security systems funded by the US National Security Agency in the 1980s but the real catalyst for active research interest in formal verification was their usage in verifying digital hardware systems. This was mainly because the cost of an uncaught design bug in hardware is much more than in software, since a silicon chip once made cannot be fixed just by releasing a patch. Instead, it has to be re-designed and re-fabricated, needing a considerable amount of time and money.
The detection of a floating-point-division bug in the Intel processor in 1994 further enhanced interest in formal hardware verification and the industry started to adopt these verification tools in their design flows from the late 1990s. With the success of formal verification methods in hardware and following some interesting developments in underlying technologies, these methods started to be used again for software analysis, in transportation and security systems. Moreover, researchers also started using powerful abstraction techniques to analyze control systems, robotics and analog circuits, and biological systems. These techniques helped reduce complexity of observable phenomena to what was relevant for a particular purpose.
Formal verification methods have recently been used to verify complete system models, along with their continuous and unpredictable physical realities. The future of formal methods seems to be quite promising as industrial leaders like Intel, Google, and Microsoft, are now actively involved in formal-methods related research.
In Pakistan, the industry has yet to initiate research and development in the area of formal verification methods. However, the academia has recognized the importance of the field. A course on formal methods is now being offered in most software engineering programs in universities across Pakistan. At the National University of Science and Technology (NUST) School of Electrical Engineering and Computer Science, we have set up a System Analysis and Verification (SAVe) lab to promote research in formal methods. Given that between 40 and 60 percent of the system development budget is spent on verifying that it meets functional and performance requirements, efficient formal verification tools and techniques can play a vital role in reducing time-to-market and ensuring accurate and reliable systems. Therefore, software companies in Pakistan should be encouraged to invest resources and efforts in this emerging trend.
About the Author:
Dr. Osman Hasan did his PhD from the Hardware Verification Group (HVG) at Concordia University in Canada. After his postdoc, Dr. Hasan joined the School of Electrical Engineering and Computer Science (SEECS) at the National University of Sciences and Technology (NUST) where he established the System Analysis and Verification (SAVe) Lab and is currently the Lab Director.