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

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

Выполните проверку свойств Simulink Design Verifier с помощью блока Proof Absulation. Он пытается доказать, что, когда сумма текущих и шести предыдущих входных значений больше 6, выходной сигнал равен 2. Модель включает блок Proof Summission, ограничивающий ввод 0 или 1. Simulink Design Verifier ищет нарушения на 20 или менее шагов времени. Он не может найти нарушение, поскольку свойство является действительным в предположении.

Найдите недопустимое свойство с помощью анализа проверки свойств Simulink Design Verifier. Он пытается доказать, что, когда сумма текущих и шести предыдущих входных значений больше 6, выходной сигнал равен 2. В этом случае свойство является недопустимым, поскольку одно большое входное значение (например, 255) приводит к тому, что сумма превышает 6. Simulink Design Verifier создает контрпример, демонстрирующий нарушение.

Выполните анализ проверки свойств с использованием опорных блоков Observer.