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