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 не определено из-за влияния приближений во время анализа.
Откройте модель sldvApproappationsExample.
Чтобы выполнить анализ генерации тестов, на вкладке Design Verifier нажмите Generate Tests. Программное обеспечение моделирует модель и проверяет результаты тестирования на соответствие данным о покрытии.
Чтобы просмотреть отчет о детальном анализе, нажмите HTML в окне Simulink Design Verifier Результатов Сводных данных.
На этом изображении показан раздел «Цели тестирования» сгенерированного отчета по анализу. Программное обеспечение предоставляет два тестов, на которые влияют приближения.
Цели тестирования состояния - цель удовлетворены
Цели тестирования статус - цель не определены с тестовыми шкафами
Чтобы выполнить анализ проверки свойств, на вкладке Design Verifier, в разделе Mode, выберите Property Proving. Нажмите Prove Properties.
На этом изображении показан раздел «Статус целей доказательства» сгенерированного отчета по анализу.
Статус целей доказательства - цель не определилась с контрпримерами
Программное обеспечение предоставляет один контрпример, на который влияют приближения.
Примечание
Th sldvApproximationsExample модель примера предварительно сконфигурирована с дополнительным анализом запуск, чтобы уменьшить образцы опции рационального приближения, установленной на Off. Если вы включите эту опцию и запустите анализ, Undecided with Testcases Цель тестирования сообщается следующим Unsatisfiable и цель доказательства сообщается следующим образом Valid.
