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