Simulink® Design Verifier™ выполняет приближения во время анализа. Программное обеспечение идентифицирует присутствие приближений и сообщает о них на уровне каждого объективного состояния в Объективной Главе Состояния отчета HTML Simulink Design Verifier. Для получения дополнительной информации смотрите Приближения Во время Анализа модели и Глав Состояния Целей.
Чтобы подтвердить тесты или контрпримеры в процессе моделирования, модель заблокирована в быстром режиме перезапуска. Для получения дополнительной информации смотрите Быструю Методологию Перезапуска.
Например, чтобы гарантировать эффект приближений, в анализе генерации тестов тесты подтверждены против данных о покрытии во время анализа.
Программное обеспечение обеспечивает тесты или контрпримеры для целей, на которые влияют из-за приближений во время анализа. Об этих целях сообщают как Цели, Нерешенные с Тестовыми сценариями для анализа генерации тестов и Целей, Нерешенных с Контрпримерами для доказывающего свойство анализа.
Программное обеспечение подтверждает цели, на которые можно повлиять из-за приближений как мертвая логика, допустимая, или невыполнимая. Эта таблица суммирует эти цели для всех аналитических режимов.
Аналитический режим | Состояние целей |
---|---|
Поиск ошибок проектирования |
|
Генерация тестов | |
Доказательство свойства |
Программное обеспечение не может подтвердить состояние целей через результаты валидации для этих случаев:
Цели введены заменой блока. Для получения дополнительной информации смотрите то, Что Замена Блока?.
Подсистема Верификации состоит из 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 сгенерированного аналитического отчета.
Состояние целей доказательства - цель, нерешенная с контрпримерами
Программное обеспечение обеспечивает один контрпример, на который влияют приближения.
Примечание
Th sldvApproximationsExample
модель в качестве примера предварительно сконфигурирована с дополнительным анализом Запуска, чтобы уменьшать экземпляры рационального набора опции приближения к Off
. Если вы включаете эту опцию и запускаете анализ, Undecided with Testcases
о цели тестирования сообщают как Unsatisfiable
и о цели доказательства сообщают как Valid
.