The MathWorks has introduced Simulink Design Verifier, which generates tests and proves design properties for Simulink and Stateflow models using the Prover Plug-In from Prover Technology.
Developers of embedded systems - especially complex or safety-critical systems - can now automatically obtain test cases to satisfy industry-standard metrics, such as modified condition/decision coverage (MC/DC), while uncovering design errors earlier in the development process when they are significantly less expensive to fix.
Simulink Design Verifier helps the simulation process by significantly reducing the need to program tests that establish complete model coverage and verify requirements. Engineers can generate test inputs that satisfy standard coverage objectives as well as user-defined test objectives and requirements.
For property proving, engineers can directly capture design requirements and performance objectives as properties in their Simulink or Stateflow models. Simulink Design Verifier mathematically proves whether those properties are satisfied and, if not, provides counterexamples that would violate the properties. As a result, engineers can find design flaws, unsatisfied requirements and unreachable states or logic that would be difficult to uncover using simulation alone.
Simulink Design Verifier performs proofs by using automated mathematical reasoning to explore model execution paths. Such systematic analysis complements simulation and provides deeper insight into the behaviour of designs.
