Библиотека блоков Simulink® Design Verifier™ включает подбиблиотеку Example Properties. Подбиблиотека Example Properties включает:
Basic Properties — Четыре примера, которые демонстрируют, как доказать основные свойства.
Temporal Properties — Четыре примера, которые демонстрируют, как задать временные свойства на булевых сигналах
Рабочий процесс для использования этих примеров в вашей модели:
Скопируйте эти примеры в свой блок 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 в пяти временных шагах.
