Using formal methods for sophisticated static code analysis
Introduction to Formal Methods
Modern static code analysis couples formal methods with error-finding techniques. Tools employing this methodology try to find errors in the source code, but they also try to prove the absence of certain critical errors. Formal methods apply theoretical computer science fundamentals to solve difficult problems in software. An example of a formal method technique is abstract interpretation, a mathematically rigorous approach to prove the absence of detectable run-time errors of software.
Abstract interpretation relies on a broad base of mathematical theorems that define rules for analyzing complex dynamic systems. Instead of analyzing each state of a program, abstract interpretation represents these states in a more general form and provides rules to manipulate them. To produce a mathematical abstraction, you need to analyze a software program's semantics.
While this idea is not new, its origins come from theory developed in the 1970s. The first implementations resulted in algorithms that grew exponentially with the size of the code. Newer algorithms address this exponential growth, and when run on today’s processors make the application of formal methods practical.
The trigonometric operation in the equation below helps explain abstract interpretation. Consider the equation in radians where x is a real number:
y = sin(2.14) + cos(0.53) + X2
For a given value of x, it is not easy to solve this equation manually without the aid of a calculator. However, if asked about the sign of the computation, you can apply the rules of trigonometry and algebra and know that the sign of the result is positive. This is true because the sin(x) >0 for x
Using the rules of trigonometry, you can precisely determine some properties of the equation. All the details are not required to make a factual and correct statement about the result.
Using the principles of abstraction as described above, you can use abstract interpretation with static code analysis to identify and diagnose run-time errors such as overflows, divide-by-zeros, and out-of-bound pointers. Metrics produced by this process provide a means to measure and improve software quality.
When applied to the detection of run-time errors, abstract interpretation completely and comprehensively provides a diagnostic of "proven," "failed," "unreachable," or "unproven" for each operation.
Loading comments... Write a comment