Verifying Code When Software Reliability Is Critical

For many embedded software projects, the primary verification goal is to find as many bugs as possible, as quickly as possible. The static analysis tools commonly used for this purpose are good at detecting flaws, but they do not prove that no errors remain in the source code. As a result, these tools do not prevent endless debugging loops and lengthy code-checking procedures. More seriously, they may leave potentially catastrophic defects undetected—unacceptable for applications that require high reliability. PolySpace code verification products provide a different approach—one that proves the absence of errors.
To prove the absence of errors, a code verification tool must exhaustively investigate every piece of code and verify its reliability against all possible data values. It must often perform tasks of a mathematical sophistication that exceeds the capabilities of a standard error-detection tool.

By Paul Barnard, Marc Lalo, and Jim Tung, The MathWorks
 
This article was published in The MathWorks News & Notes, 2008