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

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

Чтобы подтвердить тесты или контрпримеры в процессе моделирования, модель заблокирована в быстром режиме перезапуска. Для получения дополнительной информации смотрите Быструю Методологию Перезапуска (Simulink).

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

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

Программное обеспечение обеспечивает тесты или контрпримеры для целей, на которые влияют из-за приближений во время анализа. Об этих целях сообщают как Цели, Нерешенные с Тестовыми сценариями для анализа генерации тестов и Целей, Нерешенных с Контрпримерами для доказывающего свойство анализа.

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

Аналитический режимСостояние целей

Поиск ошибок проектирования

Генерация тестов

Цели, невыполнимые при приближении

Доказательство свойства

Цели, допустимые при приближении

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

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

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

В этом примере показано, как приближения влияют на состояние целей блока 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. Откройте модель sldvApproximationsExample.

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

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

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

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

    Состояние целей тестирования - цель, нерешенная с тестовыми сценариями

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

    Это изображение показывает раздел Proof Objectives Status сгенерированного аналитического отчета.

    Состояние цели доказательства - цель, нерешенная с Conterexamples

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

    Примечание

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

Похожие темы

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