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