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 сгенерированного аналитического отчета.
Программное обеспечение обеспечивает один контрпример, на который влияют приближения.
Th sldvApproximationsExample
модель в качестве примера предварительно сконфигурирована с дополнительным анализом Запуска, чтобы уменьшать экземпляры рационального набора опции приближения к Off
. Если вы включаете эту опцию и запускаете анализ, Undecided with Testcases
о цели тестирования сообщают как Unsatisfiable
и о цели доказательства сообщают как Valid
.