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