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