Simulink ® Design Verifier™ выполняет аппроксимации во время анализа. Программа определяет наличие аппроксимаций и сообщает о них на уровне каждого статуса цели в главе «Статус цели» HTML-отчета Simulink Design Verifier. Дополнительные сведения см. в разделе Аппроксимации во время анализа модели и главы состояния целей.
Для проверки тестовых примеров или контрпримеров во время моделирования модель блокируется в режиме быстрого перезапуска. Дополнительные сведения см. в разделе Методология быстрого перезапуска.
Например, чтобы обеспечить эффект аппроксимаций, в анализе генерации теста тестовые примеры проверяются на соответствие данным покрытия во время анализа.
Программное обеспечение предоставляет тестовые примеры или контрпримеры для целей, на которые влияют аппроксимации во время анализа. Эти цели указываются как цели, не определенные с помощью тестов для анализа генерации тестов, и цели, не определенные с помощью контрпримеров для анализа проверки свойств.
Программное обеспечение подтверждает цели, которые могут быть затронуты из-за аппроксимаций в качестве неактивной логики, действительных или неудовлетворительных. Эта таблица суммирует эти цели для всех режимов анализа.
| Режим анализа | Состояние целей |
|---|---|
Обнаружение ошибок конструкции |
|
Генерация тестов | |
Проверка свойств |
Программа не может подтвердить состояние целей с помощью результатов проверки для следующих случаев:
Цели, введенные заменой блока. Дополнительные сведения см. в разделе Что такое замена блоков?.
Подсистема проверки состоит из: sldv.test или sldv.prove функция.
Вы прерываете анализ при помощи кнопки Stop в окне Резюме Результатов Свидетельства Дизайна Simulink, или программное обеспечение превышает свое Максимальное аналитическое время. Поэтому некоторые цели остаются неподтвержденными во время анализа, и программное обеспечение не может подтвердить статус целей.
Блок с целью находится внутри тестового жгута Simulink, но вне тестируемого компонента. Дополнительные сведения см. в разделе Проверка связи кабелей и модели (Simulink Test).
В этой таблице приводится сводная информация о статусах целей для предыдущих случаев. Для подтверждения статуса целей необходимо выполнить дополнительное моделирование тестовых примеров или контрпримеров.
| Режим анализа | Состояние целей |
|---|---|
Обнаружение ошибок конструкции | |
Генерация тестов | |
Проверка свойств |
В этом примере показано, как аппроксимации влияют на состояние целей блока Switch. В sldvApproximationsExample модель, расчеты 1./3 и 2./3 в блоке Константа (Constant) во время анализа выполняется преобразование плавающей точки в рациональное число.
Для ввода
In2 равно -1, вход 2 блока Switch не равно 0 во время моделирования. Поэтому коммутатор не выбирает inport
In3 в качестве выходного. Для создания тестов и проверки свойств цель logical trigger input false(output is from 3rd input port) блок Switch не определился из-за влияния аппроксимаций во время анализа.
Откройте модель sldvApproximations Пример.
Для выполнения анализа генерации тестов на вкладке Design Verifier щелкните Generate Tests (Генерировать тесты). Программное обеспечение моделирует модель и проверяет результаты тестирования на соответствие данным покрытия.
Чтобы просмотреть подробный отчет об анализе, щелкните HTML в окне Сводка результатов Simulink Design Verifier.
На этом рисунке показан раздел «Состояние целей тестирования» созданного отчета об анализе. Программное обеспечение предоставляет два тестовых случая, на которые влияют аппроксимации.
Состояние целей тестирования - цель выполнена
Состояние целей тестирования - цель не определена с помощью тестов
Чтобы выполнить анализ проверки свойств, на вкладке «Проверка свойств» в разделе «Режим» выберите «Проверка свойств». Щелкните Доказать свойства.
На этом рисунке показан раздел Статус целей проверки созданного отчета об анализе.
Статус целей подтверждения - цель не определена с помощью контрпримеров
Программное обеспечение предоставляет один контрпример, на который влияют аппроксимации.
Примечание
Th sldvApproximationsExample пример модели предварительно настроен с помощью дополнительного анализа Выполнить (Run), чтобы уменьшить количество экземпляров опции рационального аппроксимации, для которой установлено значение Off. Если эта опция включена и выполняется анализ, Undecided with Testcases цель испытания сообщается как Unsatisfiable и цель доказательства сообщается как Valid.