Отчетность о приближениях через результаты валидации

Simulink® Design Verifier™ выполняет приближения во время анализа. Программа определяет наличие приближений и сообщает о них на уровне каждого объективного статуса в главе «Состояние объекта» HTML отчета Simulink Design Verifier. Для получения дополнительной информации см. «Приближения во время анализа модели и главы состояния целей».

Чтобы подтвердить тесты или контрпримеры во время симуляции, модель блокируется в режиме быстрого перезапуска. Дополнительные сведения см. в разделе Методика быстрого перезапуска.

Для примера, чтобы гарантировать эффект приближений, в анализе генерации тестов тестовые случаи проверяются на соответствие данным покрытия во время анализа.

Влияние приближений на состояние целей

Программное обеспечение предоставляет тесты или контрпримеры для целей, которые затронуты из-за приближений во время анализа. Эти цели указаны как цели, которые не были определены с помощью тестовых шкафов для анализа генерации тестов, и цели, которые не были определены с помощью контрпримеров для анализа проверки свойств.

Программное обеспечение подтверждает цели, которые могут быть затронуты из-за приближений, как мертвая логика, допустимые или неудовлетворительные. В этой таблице обобщены эти цели для всех режимов анализа.

Программное обеспечение не может подтвердить статус целей через результаты валидации для этих случаев:

  • Цели, введенные заменой блока. Для получения дополнительной информации смотрите Что такое замена блоков?.

  • Подсистема верификации состоит из sldv.test или sldv.prove функция.

  • Вы прекращаете анализ, используя кнопку Stop в окне Simulink Design Verifier Сводные Данные, или программное обеспечение превышает свое Максимальное время анализа. Поэтому некоторые цели остаются не оцененными во время анализа, и программное обеспечение не может подтвердить статус целей.

  • Блок с целью находится внутри тестовой обвязки Simulink, но вне тестируемого компонента. Для получения дополнительной информации см. «Тестовая обвязка» и «Отношение модели» (Simulink Test).

В этой таблице обобщены статусы целей для предыдущих случаев. Чтобы подтвердить статус целей, необходимо запустить дополнительные симуляции тестов или контрпримеров.

Идентифицируйте эффект приближений через результаты валидации

Этот пример показывает, как приближения влияют на статус целей блока Switch. В sldvApproximationsExample модель, вычисления 1./3 и 2./3 в блоке Constant привести к преобразованию числа с плавающей точкой в рациональное во время анализа.

Для inport In2 равно -1, а вход 2 блока Switch не равно 0 во время симуляции. Поэтому Switch не выбирает inport In3 как вывод. Для генерации тестов и анализа доказательства свойств, цель logical trigger input false(output is from 3rd input port) для блока Switch не определено из-за влияния приближений во время анализа.

  1. Откройте модель sldvApproappationsExample.

  2. Чтобы выполнить анализ генерации тестов, на вкладке Design Verifier нажмите Generate Tests. Программное обеспечение моделирует модель и проверяет результаты тестирования на соответствие данным о покрытии.

  3. Чтобы просмотреть отчет о детальном анализе, нажмите HTML в окне Simulink Design Verifier Результатов Сводных данных.

    На этом изображении показан раздел «Цели тестирования» сгенерированного отчета по анализу. Программное обеспечение предоставляет два тестов, на которые влияют приближения.

    Цели тестирования состояния - цель удовлетворены

    Цели тестирования статус - цель не определены с тестовыми шкафами

  4. Чтобы выполнить анализ проверки свойств, на вкладке Design Verifier, в разделе Mode, выберите Property Proving. Нажмите Prove Properties.

    На этом изображении показан раздел «Статус целей доказательства» сгенерированного отчета по анализу.

    Статус целей доказательства - цель не определилась с контрпримерами

    Программное обеспечение предоставляет один контрпример, на который влияют приближения.

    Примечание

    Th sldvApproximationsExample модель примера предварительно сконфигурирована с дополнительным анализом запуск, чтобы уменьшить образцы опции рационального приближения, установленной на Off. Если вы включите эту опцию и запустите анализ, Undecided with Testcases Цель тестирования сообщается следующим Unsatisfiable и цель доказательства сообщается следующим образом Valid.

Похожие темы

Для просмотра документации необходимо авторизоваться на сайте