Using formal methods for sophisticated static code analysis
Example of Formal Methods Analysis
An example of a static code analysis tool that uses formal methods with abstract interpretation is the Polyspace code verifier from MathWorks. This code verification tool consumes source files written in the C, C++, or Ada programming language to identify where certain run-time errors occur and to prove their absence.
The verification process starts by first identifying places in source files that might fail with a run-time error. Then using abstract interpretation, the tool classifies every error as unproven, and subsequently attempts to prove that the code will fail, is unreachable, or is proven not to fail. Using a color-coding scheme as shown in Figure 1 below, the tool identifies the status of operations in the code.
Click on image to enlarge.
Code elements identified in green are proven to be free of certain run-time errors such as overflow, divide-by-zero, illegally dereferenced pointers, and other run-time errors. Operations marked in red show places where Polyspace has detected run-time errors. Those operations that might fail under some conditions are marked in orange. Code elements or conditional branches that cannot be executed (dead code or unreachable code) are marked in gray.
Next, consider how Polyspace analyzes the results of the code fragment shown earlier. As shown in Figure 2 below, Polyspace marks the divide operation in green, indicating that this code operation will not result in a divide by zero (because of the ranges of the variable a is 43 .. 727 and never zero).
Click on image to enlarge.
Detailed interprocedural static code analysis using abstract interpretation determines that this variable will never be equal to zero.
Conclusion
Static code analysis that is augmented with formal methods (abstract interpretation) can be an important tool for improving the quality of embedded software used in high-integrity software systems. A software development process that includes these types of static code analysis tools can contribute to attaining a good quality process. Using this approach helps software developers and verification engineers assess the quality and safety of their production software.
Jay Abraham is a product marketing manager with responsibility for Polyspace code verification products at Mathworks. His area of expertise is in software tools for the verification of critical embedded applications. His 20 years of experience include engineering and design positions at hardware, software tools, and embedded operating systems companies including Magma Design Automation and Wind River Systems; he began his career as a microprocessor designer at IBM. Jay has an M.S. in computer engineering from Syracuse University and a B.S. in electrical engineering from Boston University.
Loading comments... Write a comment