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