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