Приближения

Приближения во время анализа модели

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:

  • Параметром Interpolation method является Linear.

  • Параметром Extrapolation method является Clip или Linear.

  • Ввод и вывод сигнализирует, что у обоих есть тип данных с плавающей точкой.

Приближение одного - и двумерные интерполяционные таблицы для целого числа и типов данных с фиксированной точкой

Если ваша модель содержит интерполяционные таблицы следующих характеристик, Simulink Design Verifier автоматически преобразует вашу исходную интерполяционную таблицу в новую интерполяционную таблицу, состоявшую из точек останова, которые равномерно расположены с интервалами в каждой из их соответствующих размерностей.

БлокХарактеристики

Блок n-D Lookup Table, n = 1 или n = 2:

  • Параметром Interpolation method является Linear.

  • Параметром Extrapolation method является Clip .

  • Параметром Index search method является Linear search или Binary search.

  • Сигналы ввода и вывода и имеют тот же тип и являются оба целочисленным типом или фиксированной точкой.

Это приближение позволяет Simulink Design Verifier генерировать тесты значительно быстрее. Сохраненное время объявлено, когда у вас есть невыполнимые цели тестирования в вашей модели.

Если Simulink Design Verifier применяет такие приближения к вашей модели, отчет Simulink Design Verifier включает в себя детали приближения.

Циклы с условием продолжения

Если ваша модель или Stateflow® график в вашей модели содержит while цикл, Simulink Design Verifier пытается обнаружить консервативную константу, связанную, который позволяет while цикл, чтобы выйти. Если программное обеспечение не может найти константу связанной, оно выполняет while приближение цикла. Этим приближением анализ не доказывает цели быть допустимым или невыполнимым, и это не доказывает мертвую логику. Сгенерированный аналитический отчет отмечает это приближение.

Поведение while приближение цикла сопоставимо во всех режимах анализа, как описано в следующей таблице.

Аналитический режимПриближение цикла с условием продолжения
Поиск ошибок проектированияОпределяет номер while итерации цикла к 3. Не сообщают мертвая логика или допустимые цели.
Генерация тестаОпределяет номер while итерации цикла к 3. Не сообщают невыполнимые цели.
Доказательство свойстваОпределяет номер while итерации цикла к 3. Не сообщают допустимые цели.
Для просмотра документации необходимо авторизоваться на сайте