Требования к модели
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 в течение пяти временных шагов.
