Simulink® Design Verifier™ программного обеспечения пытается сгенерировать входы и параметры для достижения целей. Однако может быть бесконечное количество значений для поиска программного обеспечения. Чтобы создать разумные пределы на анализ, программное обеспечение выполняет приближения, чтобы упростить анализ. Программное обеспечение регистрирует любые приближения, выполненные в главе «Аналитическая информация» HTML-отчета Simulink Design Verifier. Описание этой главы см. в разделе «Информация об анализе».
Внимательно просмотрите результаты анализа, когда программное обеспечение использует приближения. Оцените свою модель, чтобы определить, какие блоки или подсистемы заставили программное обеспечение выполнять приближения.
Редко приближение может привести к тестам, которые не достигают целей тестирования или демонстрируют ошибку проектирования, или контрпримерам, которые не могут фальсифицировать цели доказательства. Например, предположим, что программное обеспечение генерирует сигнал теста, который должен достичь цели путем превышения порога; ошибка округления с плавающей точкой может помешать этому сигналу достичь порогового значения.
Программное обеспечение Simulink Design Verifier выполняет следующие приближения при анализе модели:
В некоторых случаях программное обеспечение Simulink Design Verifier упрощает линейную арифметику чисел с плавающей запятой, аппроксимируя их рациональными числами с бесконечной точностью. Программа обнаруживает, как логические отношения между этими значениями влияют на цели. Этот анализ позволяет программному обеспечению поддерживать диспетчерскую логику, которая обычно встречается во встроенных проектах элементов управления.
Если ваша модель содержит значения с плавающей точкой в сигналах, входных значениях или параметрах блоков, Simulink Design Verifier преобразует некоторые значения в рациональные числа перед выполнением своего анализа. В результате этих приближений:
Ошибка округления не учитывается.
Верхняя и нижняя границы чисел с плавающей запятой не рассматриваются.
Если ваша модель приведет значения с плавающей точкой к целым значениям, представление целого числа может повлиять на тесты, сгенерированные для модели. В некоторых редких случаях сгенерированные тесты могут не удовлетворять целям, связанным со значениями с плавающей точкой.
Программное обеспечение Simulink Design Verifier не поддерживает нелинейную арифметику для типов данных с плавающей точкой. Если ваша модель содержит какие-либо 2-D Lookup Table блоки или n-D Lookup Table блоки, где n = 2, со всеми следующими характеристиками, программа аппроксимирует нелинейную двумерную интерполяцию с линейной интерполяцией путем подбора плоскостей к каждому интерполяционному интервалу.
| Блок | Особенности |
|---|---|
n-D Lookup Table блок, n = 2: |
|
Если ваша модель содержит интерполяционные таблицы следующих характеристик, Simulink Design Verifier автоматически преобразует исходную интерполяционную таблицу в новую интерполяционную таблицу, состоящую из точек прерывания, которые равномерно разнесены в каждом из соответствующих размерностей.
| Блок | Особенности |
|---|---|
n-D Lookup Table блок, n = 1 или n = 2: |
|
Это приближение позволяет Simulink Design Verifier генерировать тесты значительно быстрее. Время экономии выражается, когда у вас в модели есть неудовлетворительные цели тестирования.
Если Simulink Design Verifier применяет такие приближения к вашей модели, отчет Simulink Design Verifier включает детали аппроксимации.
Если ваша модель или Stateflow® график в вашей модели содержит while цикл, Simulink Design Verifier пытается обнаружить консервативную постоянную границу, которая позволяет while цикл для выхода. Если программа не может найти постоянную границу, она выполняет while цикл приближения. При таком приближении анализ не доказывает, что цели действительны или неудовлетворительны, и не доказывает мертвой логики. Сгенерированный отчет анализа отмечает это приближение.
Поведение while цикл приближения согласован во всех режимах анализа, как описано в следующей таблице.
| Режим анализа | Цикл While Приближения |
|---|---|
| Поиск ошибок проектирования | Устанавливает количество while Итерации цикла к 3. Не сообщает о мертвой логике или допустимых целях. |
| Тест | Устанавливает количество while Итерации цикла к 3. Не сообщает о неудовлетворительных целях. |
| Проверка свойств | Устанавливает количество while Итерации цикла к 3. Не сообщает о допустимых целях. |