Simulink® Design Verifier™ выполняет приближения во время анализа. Программное обеспечение идентифицирует присутствие приближений и сообщает о них на уровне каждого объективного состояния в Объективной Главе Состояния отчета HTML Simulink Design Verifier. Для получения дополнительной информации смотрите Приближения Во время Анализа модели и Глав Состояния Целей.
Чтобы подтвердить тесты или контрпримеры во время симуляции, модель заблокирована в быстром режиме перезапуска. Для получения дополнительной информации смотрите Быструю Методологию Перезапуска (Simulink).
Например, чтобы гарантировать эффект приближений, в анализе генерации тестов тесты подтверждены против данных о покрытии во время анализа.
Программное обеспечение обеспечивает тесты или контрпримеры для целей, на которые влияют из-за приближений во время анализа. Об этих целях сообщают как Цели, Нерешенные с Тестовыми сценариями для анализа генерации тестов и Целей, Нерешенных с Контрпримерами для доказывающего свойство анализа.
Программное обеспечение подтверждает цели, на которые можно повлиять из-за приближений как мертвая логика, допустимая, или невыполнимая. Эта таблица суммирует эти цели для всех аналитических режимов.
| Аналитический режим | Состояние целей |
|---|---|
Поиск ошибок проектирования |
|
Генерация тестов | |
Доказательство свойства |
Программное обеспечение не может подтвердить состояние целей через результаты валидации для этих случаев:
Цели введены заменой блока. Для получения дополнительной информации смотрите то, Что Замена Блока?.
Подсистема Верификации состоит из функции sldv.prove или sldv.test.
Вы прерываете анализ при помощи кнопки Stop в окне Simulink Design Verifier Results Summary, или программное обеспечение превышает свое Максимальное аналитическое время. Поэтому некоторые цели остаются неподтвержденными во время анализа, и программное обеспечение не может подтвердить состояние целей.
Блок с целью в тестовой обвязке Simulink, но вне компонента под тестом. Для получения дополнительной информации смотрите Тестовую обвязку и Отношение Модели (Simulink Test).
Эта таблица суммирует состояния целей для предыдущих случаев. Чтобы подтвердить состояние целей, необходимо запустить дополнительные симуляции тестов или контрпримеров.
| Аналитический режим | Состояние целей |
|---|---|
Поиск ошибок проектирования | |
Генерация тестов | |
Доказательство свойства |
Этот пример показывает, как приближения влияют на состояние целей блока switch. В модели sldvApproximationsExample вычисления 1./3 и 2./3 в блоке Constant приводят к С плавающей точкой к Преобразованию Рационального числа во время анализа.
Для импорта
In2, равный -1, вход 2 блока switch не равен 0 во время симуляции. Поэтому Переключатель не выбирает, импортируют
In3, как выведено. Для генерации тестов и доказывающего свойство анализа, объективный logical trigger input false(output is from 3rd input port) для блока switch не решен из-за влияния приближений во время анализа.
Откройте модель sldvApproximationsExample.
Для анализа генерации тестов нажмите Analysis> Design Verifier> Generate Tests> Model. Программное обеспечение моделирует модель и подтверждает результаты испытаний против данных о покрытии.
Чтобы просмотреть отчет детального анализа, нажмите HTML в окне Simulink Design Verifier Results Summary.
Это изображение показывает раздел Test Objectives Status сгенерированного аналитического отчета. Программное обеспечение обеспечивает два теста, на которые влияют приближения.
Для анализа доказательства свойства нажмите Analysis> Design Verifier> Prove Properties> Model.
Это изображение показывает раздел Proof Objectives Status сгенерированного аналитического отчета.
В модели sldvApproximationsExample в качестве примера по умолчанию дополнительным анализом Выполнения, чтобы уменьшать экземпляры рациональной опции приближения является On. Из-за этого дополнительного анализа, о Состоянии Целей доказательства сообщают как Objectives Valid.
Просмотреть влияние рационального приближения согласно анализу доказательства свойства:
В диалоговом окне Configurations Parameters, на панели Design Verifier, в Advanced parameters, снимают флажок для Запущенного дополнительного анализа, чтобы уменьшать экземпляры рационального приближения. Чтобы применить эту установку, нажмите OK.
Для анализа доказательства свойства нажмите Analysis> Design Verifier> Prove Properties> Model.
Это изображение показывает раздел Proof Objectives Status сгенерированного аналитического отчета.
Программное обеспечение обеспечивает один контрпример, на который влияют приближения.
