Программное обеспечение 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 итерации цикла к 3. Не сообщают мертвая логика или допустимые цели. |
| Генерация теста | Определяет номер while итерации цикла к 3. Не сообщают невыполнимые цели. |
| Доказательство свойства | Определяет номер while итерации цикла к 3. Не сообщают допустимые цели. |