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.
