Simulink Design Verifier

Formal Methods in Model-Based Design

Simulink Design Verifier uses formal analysis techniques provided by the Prover Plug-In from Prover Technology and the Polyspace formal analysis engine from MathWorks. These techniques rely on mathematically rigorous procedures to search through the possible execution paths of your model for test cases and counterexamples. Unlike traditional testing methods in which test scenarios and expected results are expressed with concrete data values, formal analysis techniques let you work with models of system behavior instead of concrete data values. A model of system behavior can include models of 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.