В этом примере показано, как проверить модель проекта напоминания о ремне безопасности, на которую ссылаются в главном блоке выше. Блок Safety Properties ниже его содержит свойство, заданное в Таблице истинности MATLAB, которая указывает, когда SeatBeltIcon выход должен быть активным. Simulink Design Verifier анализирует модель проекта и свойство безопасности доказать правильность или идентифицировать контрпримеры. В этой модели свойство доказано под явным предположением, что вход KEY запускается в 0 и изменяется шагом 1.
open_system('sldvexSBRVerificationTruthTableFixedExample');
