Property Proving Using MATLAB Truth Table Block

This example shows how to verify the seat belt reminder design model referenced in the top block above. The Safety Properties block below it contains a property specified in MATLAB Truth Table that indicates when the SeatBeltIcon output 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 proven under the explicit assumption that the KEY input starts at 0 and changes by increments of 1.

open_system('sldvexSBRVerificationTruthTableFixedExample');