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 all possible execution paths of your model or code base to identify errors in your design.
You can perform formal verification on models and on code generated from these models.
You can employ formal verification methods to identify errors in your model and generates test vectors that reproduce the error 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 performed with such models complements simulation and provides a deeper understanding of your design.
For details see Simulink Design Verifier™.
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.
See also: static code analysis, Simulink Design Verifier, Polyspace products, Simulink Verification and Validation, embedded systems, formal verification videos, requirements tracebility, model based testing