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