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