Некоторые характеристики моделей Simulink ® могут вызвать проблемы при анализе Verifier™ Simulink Design следующими способами:
Сложность входных данных модели из-за:
Большое количество исходных данных (Количество исходных данных может измениться, в зависимости от отдельной модели.)
Типы входных данных (например, значения с плавающей запятой)
Способ влияния входных данных на состояние модели и цели анализа
Количество возможных путей моделирования в модели
Части модели, которые не могут быть достигнуты
Большие счетчики в модели
В разделах «Снижение сложности» описываются методы, предназначенные для уменьшения влияния этой сложности и достижения максимальной производительности от Simulink Design Verifier.
Большинство этих методов сосредоточено на создании тестов для больших моделей. Однако многие из них можно использовать для обнаружения ошибок конструкции или подтверждения свойств большой модели и создания контрпримеров при отмене свойства. Кроме того, Докажи свойства в больших моделях описывает конкретные методы для доказательства свойств в большой модели.