Formal verification helps confirm that your embedded system software models and code behave correctly. These 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.
Using Simulink Design Verifier and Polyspace software products, you can perform formal verification on models designed in MATLAB and Simulink and on code generated from these models.
Simulink Design Verifier employs 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.
Polyspace products use static code analysis and formal verification methods 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.