What Are Formal Methods?

Formal methods apply theoretical computer science fundamentals to solve difficult problems in software, such as proving that software will not fail with a run-time error. An example is abstract interpretation, a mathematically rigorous approach to prove the correctness of software. Formal methods for verification purposes (also known as formal verification) can help improve software reliability and robustness.

Traditional methods of software verification rely on testing to verify behavior and robustness, but testing can only show the presence of errors—not their absence. In contrast, formal methods use mathematics to prove certain facts or properties. Therefore, verification techniques based on formal methods can conclusively prove certain attributes of software, such as proving that software does or does not contain run-time errors including overflows, divide-by-zero, and illegally dereferenced pointers.

Use formal methods coupled with static code analysis to perform code verification to identify and diagnose run-time errors. Use the metrics produced by this process to measure and improve software quality. Because formal methods-based static code analysis is automated, you can do this analysis without executing the software or developing test cases.

You can use static analysis tools that use formal methods for the following tasks:

• Detecting elusive run-time errors
• Proving the absence of certain run-time errors
• Producing code quality metrics and checking source code for compliance to code standards such as MISRA C and JSF++

With this comprehensive, complete approach, you can identify every failure point in the code as proven to fail, proven not to fail, may never execute (dead code), or unproven. Abstract interpretation was first used to verify software for the Ariane 5 launch vehicle to detect an overflow error converting a 64-bit floating point variable to a signed 16-bit integer. It is the first example of large-scale static code analysis by formal methods-based abstract interpretation.

For details, see Polyspace^® products.