Требования модели

Библиотека блоков Simulink® Design Verifier™ включает подбиблиотеку Example Properties. Подбиблиотека Example Properties включает:

  • Basic Properties — Четыре примера, которые демонстрируют, как доказать основные свойства.

  • Temporal Properties — Четыре примера, которые демонстрируют, как задать временные свойства на булевых сигналах

Рабочий процесс для использования этих примеров в вашей модели:

  1. Скопируйте эти примеры в свой блок Verification Subsystem.

  2. Адаптируйте их при необходимости к определенным свойствам, которые вы хотите доказать.

  3. Запустите анализ Simulink Design Verifier, чтобы доказать, что утверждения в этих примерах никогда не перестали работать.

  4. Если утверждение перестало работать, программное обеспечение создает контрпример, который заставляет утверждение перестать работать и затем генерирует модель тестовой обвязки.

  5. На модели тестовой обвязки выполните контрпример, чтобы подтвердить, что утверждение перестало работать с тем контрпримером.

Основные свойства

Просмотреть примеры Basic Properties:

  1. Откройте библиотеку блоков Simulink Design Verifier. Ввод:

    sldvlib
  2. Дважды кликните подбиблиотеку Examples.

  3. Дважды кликните блок Basic Properties, который содержит примеры.

Разделы, которые следуют, описывают каждый пример в подбиблиотеке Block Properties подробно.

Условия, который Триггер Результат

Блок Simulink Design Verifier Implies позволяет вам тестировать на условия, которые инициировали результат. Этот пример задает это если условие A верно, результат B должно всегда быть верным.

Увеличение или уменьшение сигналов

Эти два примера в этом разделе указывают, что сигнал также:

  • Всегда увеличиваясь или оставаясь постоянным

  • Всегда уменьшаясь или оставаясь постоянным

Операция исключительности

Этот пример описывает четыре условия, которые не должны быть верными одновременно.

Условия с одним истинным элементом

Этот пример указывает, что только один из этих четырех входных сигналов может быть верным.

Временные свойства

Просмотреть примеры Temporal Properties:

  1. Откройте библиотеку блоков Simulink Design Verifier. Ввод:

    sldvlib
  2. Дважды кликните подбиблиотеку Temporal Properties.

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

Похожие темы

Для просмотра документации необходимо авторизоваться на сайте