Simulink ® Design Verifier™ analysis ищет последовательности состояний, чтобы найти входные значения, которые приводят анализ к состоянию, удовлетворяющему цели. Каждое значение счетчика или шаг таймера соответствует различному состоянию, так что наличие длительных таймеров или счетчиков может резко увеличить размер представления состояния. Поскольку сложность анализа зависит от размера представления состояния, необходимо уделить особое внимание счетчикам и таймерам в модели, чтобы избежать усложнения анализа Simulink Design Verifier.
Примечание
Для целей анализа Simulink Design Verifier термин «конфигурация» относится к набору значений для всей постоянной информации в модели.
Процесс поиска исследует все конфигурации, которые могут быть достигнуты за один шаг таймера, прежде чем рассматривать любую из конфигураций, которые могут быть достигнуты за два шага таймера. Аналогично, поиск исследует все конфигурации, которые могут быть достигнуты за два шага таймера, прежде чем рассматривать любую конфигурацию, которая требует трех или более шагов таймера, и так далее. Количество шагов таймера, необходимых для исчерпания счетчика, напрямую влияет на количество состояний, которые необходимо искать в анализе. Модели, содержащие временные задержки, такие как таймеры обратного отсчета, усложняют анализ, заставляя поиск охватывать большое количество состояний.
Подобные эффекты могут наблюдаться, когда системы используют интенсивное усреднение и фильтрацию для задержки реакции на изменение входных данных. Любой аспект конструкции, который задерживает ответ, приводит к тому, что тестовые последовательности содержат больше шагов таймера, что приводит к более длинным тестовым случаям, которые сложнее идентифицировать.
Ниже перечислены некоторые основные методы, которые можно использовать для повышения производительности анализа в моделях со счетчиками или таймерами.
Выберите очень малые значения для временных задержек. Система с логической ошибкой, когда временная задержка установлена на 2000 шагов, обычно демонстрирует эту ошибку, если временная задержка изменена на 2 шага. Если система имеет несколько задержек, выберите небольшие, но уникальные значения для каждой из них, чтобы задержки постепенно удовлетворялись.
Задайте начальные значения счетчиков и параметров таймеров, которые может изменить Simulink Design Verifier. Программа находит начальные значения, которые позволяют более коротким тестовым случаям превышать пороговые значения. Дополнительные сведения см. в разделе Значения ограничений параметров.
Выберите более высокие частотные отсечки для фильтров и меньшее количество отсчетов для усреднения, чтобы минимизировать задержки фильтрации.
Некоторые из более совершенных методов, которые можно использовать для повышения производительности анализа в моделях со счетчиками или таймерами, включают следующие:
Использовать sldvtimer для определения шаблонов таймеров, которые можно оптимизировать для создания тестов Simulink Design Verifier.
Используйте существующий тестовый случай или набор тестовых случаев, который исчерпывает счетчик или таймер, и расширьте эти тестовые случаи, чтобы создать полный набор тестов. Дополнительные сведения см. в разделе Определение и расширение существующих тестов.