What Is Formal Verification?

Formal verification helps confirm that your embedded system software models and code behave correctly. Formal verification methods rely on mathematically rigorous procedures to search through possible execution paths of your model or code to identify errors in your design. You can perform formal verification on models, generated code, and hand code.

Formal Verification of Models

Formal verification helps you identify errors in your model and generate test vectors that reproduce errors in simulation. Unlike traditional testing methods in which expected results are expressed with concrete data values, formal verification techniques let you work on models of system behavior. Such models can include test scenarios and verification objectives that describe desired and undesired system behaviors. Formal analysis complements simulation and provides a deeper understanding of your design.

For details see Simulink Design Verifier™.

Formal Verification of Code

Using static code analysis and formal verification methods, you can use tools to detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in source code written in C/C++ or Ada. You can use them to perform code verification of handwritten or generated embedded software. You can also check compliance to coding standards, review code complexity metrics, and measure software quality.

For details, see Polyspace^® products.