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