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