Библиотека блоков Simulink ® Design Verifier™ содержит подзаголовок «Свойства примера». Поддиапазон «Свойства примера» включает в себя:
Основные свойства - четыре примера, демонстрирующих, как доказать основные свойства.
Временные свойства - четыре примера, демонстрирующие, как определять временные свойства для логических сигналов
Поток операций для использования этих примеров в модели:
Скопируйте эти примеры в блок подсистемы проверки.
При необходимости адаптируйте их для определенных свойств, которые вы хотите доказать.
Выполните анализ Simulink Design Verifier, чтобы доказать, что утверждения в этих примерах никогда не выходят из строя.
Если утверждение завершается неуспешно, программа создает контрпример, который приводит к сбою утверждения, а затем создает модель электрического жгута.
В модели кабельных трасс выполните контрпример, чтобы подтвердить, что утверждение не соответствует этому контрпримеру.
Чтобы просмотреть примеры основных свойств:
Откройте библиотеку блоков Simulink Design Verifier. Тип:
sldvlib
Дважды щелкните по подзаголовку Примеры.
Дважды щелкните блок «Основные свойства», содержащий примеры.
Следующие разделы подробно описывают каждый пример в подстранице «Свойства блока».
Блок Simulink Design Verifier Improves позволяет проверить наличие условий, запускающих результат. В этом примере указывается, что если условие A true, результат B всегда должно быть правдой.
Два примера в этом разделе указывают, что сигнал:
Всегда увеличивается или остается постоянным
Всегда уменьшается или остается постоянным
В этом примере описываются четыре условия, которые не должны выполняться одновременно.
В этом примере указывается, что истинным может быть только один из четырех входных сигналов.
Чтобы просмотреть примеры временных свойств:
Откройте библиотеку блоков Simulink Design Verifier. Тип:
sldvlib
Дважды щелкните по поддиапазону «Временные свойства».
Дважды щелкните блок «Временные свойства», содержащий примеры.
Следующие разделы подробно описывают каждый пример в подстранице «Временные свойства».
Когда вход In1 равняется ACTIVE, вход In2 имеет значение INACTIVE через пять временных шагов.
В этом примере, после пяти последовательных временных шагов, где SENSOR_HIGH вход имеет значение true, поле CMD сигнал становится истинным. CMD является истинным до тех пор, пока SENSOR_HIGH true, если блок не сброшен MANUAL_RESET сигнал.
В этом примере после того, как вход становится истинным, выход становится истинным для количества временных шагов, указанных в блоке детектора, в данном случае 5. Ввод также остается верным в течение 5 временных шагов.
Когда вход In3 равняется ON и вход In4 меньше константы THRESHOLD, In3 имеет значение OFF в течение пяти временных шагов.
