Проект Панели верификатора: проверка свойств
Обзор панели проверки свойств
Задайте опции, которые управляют тем, как Simulink® Design Verifier™ доказывает свойства для моделей, которые он анализирует.
См. также
Блоки утверждения
Укажите, включены ли или отключены блоки Assertion в модели.
Настройки
По умолчанию: Use local settings
Use local settingsВключает или отключает блоки Assertion зависимости от значения параметра Enable каждого блока. Если выбран Enable параметр блока, блок активируется; в противном случае блок отключен.
Enable allВключает все блоки Assertion в модели независимо от настроек их параметров Enable.
Disable allОтключает все блоки Assertion в модели независимо от настроек их параметров Enable.
Информация о командной строке
Параметр: DVAssertions |
| Тип: символьный массив |
Значение: 'UseLocalSettings' | 'EnableAll' | 'DisableAll' |
По умолчанию: 'UseLocalSettings' |
См. также
Доказательства допущений
Укажите, включены ли или отключены блоки Proof Assumption в модели.
Настройки
По умолчанию: Use local settings
Use local settingsВключает или отключает блоки Proof Assumption зависимости от значения параметра Enable каждого блока. Если выбран Enable параметр блока, блок активируется; в противном случае блок отключен.
Enable allВключает все блоки Proof Assumption в модели независимо от настроек их параметров Enable.
Disable allОтключает все блоки Proof Assumption в модели независимо от настроек их параметров Enable.
Информация о командной строке
Параметр: DVProofAssumptions |
| Тип: символьный массив |
Значение: 'UseLocalSettings' | 'EnableAll' | 'DisableAll' |
По умолчанию: 'UseLocalSettings' |
См. также
Стратегия
Укажите стратегию, которую Simulink Design Verifier использует при проверке свойств.
Настройки
По умолчанию: Prove
ProveВыполняет проверку свойств.
FindViolationПоиск только нарушений свойств в пределах количества шагов симуляции, заданных опцией Maximum violation steps.
ProveWithViolationDetectionИщет как нарушения собственности, так и пытается доказать свойства, по которым не удалось обнаружить нарушение. Эта стратегия является относительно оптимальным балансом между
ProveWithViolationDetectionиFindViolationстратегии.
Зависимость
Выбор FindViolation или ProveWithViolationDetection включает параметр Maximum violation steps.
Информация о командной строке
Параметр: DVProvingStrategy |
| Тип: символьный массив |
Значение: 'Prove' | 'FindViolation' | 'ProveWithViolationDetection' |
По умолчанию: 'Prove' |
См. также
Максимальные шаги нарушения
Задайте максимальное количество шагов симуляции, на которых Simulink Design Verifier ищет нарушения свойств.
Настройки
По умолчанию: 20
Программа Simulink Design Verifier не ищет больше заданного максимального количества шагов симуляции. Поэтому он не может идентифицировать нарушения, которые могут произойти позже в симуляции.
Зависимость
Этот параметр активируется, когда вы задаете Strategy FindViolation или ProveWithViolationDetection.
Информация о командной строке
Параметр: DVMaxViolationSteps |
Тип: int32 |
| Значение: любое допустимое значение |
По умолчанию: 20 |