Formal Methods

Proving that software will not fail with a run-time error

Formal methods apply theoretical computer science fundamentals to solve difficult problems in software, such as proving that the software will not fail with a run-time error. An example is abstract interpretation, a mathematically rigorous approach to prove 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.

You 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.

Together, formal methods and static code analysis let you:

• Detect elusive run-time errors
• Prove the absence of certain run-time errors

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. This technique 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.

Polyspace products are static analysis tools that use formal methods. They perform static analysis to detect run-time errors and prove the absence of certain run-time errors in C/C++ and Ada source code. They also produce code quality metrics and check source code for compliance to code standards such as MISRA-C/C++ and JSF++.

Examples and How To

• Eliminating Critical Software Errors in Embedded Code Using Static Code Analysis (Webinar)
• Proving the Absence of Run-Time Errors 3:44 (Video)

Software Reference

• Polyspace Client for C/C++ (Product)
• Polyspace Client for Ada (Product)

See also: Polyspace code verification products, verification, validation, and test, embedded systems