Property Proving Using MATLAB Function Block

This example shows how to verify the seat belt reminder design model. The Safety Properties block below it contains a property specified in MATLAB® that indicates when the icon should be active. Simulink® Design Verifier™ analyzes the design model and safety property to prove correctness or to identify counterexamples. In this model, the property is violated because the design implicitly assumes that the KEY input starts at 0 and changes by increments of 1.

open_system('sldvdemo_sbr_verification');