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

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

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

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

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

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

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

Аналитический режим	Состояние целей
Поиск ошибок проектирования	Мертвая логика при приближении Цели, допустимые при приближении
Генерация тестов	Цели, невыполнимые при приближении
Доказательство свойства	Цели, допустимые при приближении

Аналитический режим

Состояние целей

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

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

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

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

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

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

Цели введены заменой блока. Для получения дополнительной информации смотрите то, Что Замена Блока?.
Подсистема Верификации состоит из sldv.test или sldv.prove функция.
Вы прерываете анализ при помощи кнопки Stop в окне Simulink Design Verifier Results Summary, или программное обеспечение превышает свое Максимальное аналитическое время. Поэтому некоторые цели остаются неподтвержденными во время анализа, и программное обеспечение не может подтвердить состояние целей.
Блок с целью в тестовой обвязке 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 блок не решен из-за удара приближений во время анализа.

Откройте модель sldvApproximationsExample.
Чтобы выполнить анализ генерации тестов, на вкладке Design Verifier, нажимают Generate Tests. Программное обеспечение симулирует модель и подтверждает результаты испытаний против данных о покрытии.
Чтобы просмотреть отчет детального анализа, нажмите HTML в окне Simulink Design Verifier Results Summary.
Это изображение показывает раздел Test Objectives Status сгенерированного аналитического отчета. Программное обеспечение обеспечивает два теста, на которые влияют приближения.
Состояние целей тестирования - удовлетворенная цель
Состояние целей тестирования - цель, нерешенная с тестовыми сценариями
Чтобы выполнить анализ доказательства свойства, на вкладке Design Verifier, в разделе Mode, выбирают Property Proving. Нажмите Prove Properties.
Это изображение показывает раздел Proof Objectives Status сгенерированного аналитического отчета.
Состояние цели доказательства - цель, нерешенная с Conterexamples
Программное обеспечение обеспечивает один контрпример, на который влияют приближения.
Примечание
Th sldvApproximationsExample модель в качестве примера предварительно сконфигурирована с дополнительным анализом Запуска, чтобы уменьшать экземпляры рационального набора опции приближения к Off. Если вы включаете эту опцию и запускаете анализ, Undecided with Testcases о цели тестирования сообщают как Unsatisfiable и о цели доказательства сообщают как Valid.

Документация