Докажите свойства уровня системы Используя модель верификации

Когда использовать модель верификации в доказательстве свойства

Если ваша модель имеет свойства в масштабе всей системы, которые влияют на поведение модели, вы можете хотеть доказать свойства, не изменяя модель проекта. Для этого вы создаете verification model, который включает:

Блок Model это ссылается на модель проекта
Одна или несколько подсистем верификации, которые задают свойства и любые необходимые ограничения

Об этом Примере

Модель проекта sldvdemo_sbr_design моделирует логику для света напоминания о ремне безопасности. Если воспламенение включено, ремни безопасности откреплены, и автомобиль превышает определенную скорость, свет напоминания о ремне безопасности включает.

sldvdemo_sbr_verification модель является моделью верификации, которая задает некоторые ограничения и проверяет свойства в sldvdemo_sbr_design модель. Блок Model в моделях - ссылках верификации модель проекта, так, чтобы логика верификации существовала только в модели верификации.

sldvdemo_sbr_verification модель содержит свойство, которое сфальсифицировано, потому что ограничение отключено. В sldvdemo_sbl_verification_fixed модель, ограничение включено, и все свойства доказаны допустимыми.

Изучите модель верификации

Сделайте эти шаги, чтобы изучить, как модель верификации работает:

Откройте модель верификации:
```
sldvdemo_sbr_verification
```
Блок Design Model является блоком Model, это ссылается на sldvdemo_sbr_design. График SBR Stateflow^® в модели проекта принимает что KEY вход первоначально 0.
Откройте подсистему Safety Properties, которая задает свойства модели проекта, которую вы хотите доказать.
Эта подсистема содержит блок MATLAB Function под названием MATLAB Property. Код в этом блоке задает свойство, что напоминание о ремне безопасности должно быть включено, когда воспламенение включено, ремень безопасности не закрепляется, и скорость меньше 15:
Закройте подсистему Safety Properties.
Откройте Входную Ограничительную подсистему.
Эта подсистема задает следующие ограничения:
- Ключ может иметь три положения: 0, 1, 2
- Скорость ограничивается упасть между 10 и 30.
- Ключ должен запуститься в 0 и может только измениться одним шагом за один раз. Например, ключ может измениться с 0 до 1 или 1 - 2, но не с 0 до 2. В этой модели верификации не включено это ограничение.
Закройте Входную Ограничительную подсистему, но сохраните sldvdemo_sbr_verification открытая модель.

Докажите свойства модели проекта

Анализируйте sldvdemo_sbr_verification модель, чтобы доказать свойства:

В sldvdemo_sbr_verification окно модели, чтобы запустить анализ, дважды кликает кнопку Run, чтобы запустить анализ.
Когда анализ завершается, логарифмическое окно Simulink^® Design Verifier™ указывает, что одна цель сфальсифицирована - симуляция потребностей. Для получения дополнительной информации смотрите Сфальсифицированные Цели - Симуляция Потребностей.
Чтобы видеть, какая цель была сфальсифицирована, нажмите Highlight analysis results on model.
Подсистема Safety Properties подсвечена в оранжевом.
Откройте подсистему Safety Properties и кликните по блоку MATLAB Property.
Окно Simulink Design Verifier Results указывает что оператор
```
sldv.prove(implies(activeCond,SeatBeltIcon))
```
было ложным по крайней мере во время одного временного шага.
Нажмите View counterexample, чтобы видеть значения сигналов, которые нарушили это свойство.
Блок Signal Builder открывается контрпримером. KEY вход равнялся первоначально 2, который недопустим.

Подтверждать свойство задало в подсистеме Safety Properties, необходимо убедиться что начальное значение KEY 0.

Зафиксируйте модель верификации

Входная Ограничительная подсистема в модели верификации содержала три ограничения. Третье ограничение, которое требует что начальное значение KEY будьте 0, и тот KEY может только измениться с шагом 1, отключен.

Чтобы видеть, как это свойство подтверждено, когда вы включаете третье ограничение:

В sldvdemo_sbr_verification модель, нажмите Open Fixed Model.
sldvdemo_sbr_verification_fixed модель верификации открывается.
Откройте Входную Ограничительную подсистему.
Это третье ограничение теперь включено так, чтобы KEY имеет начальное значение 0 и изменяется с шагом 1.
Закройте Входную Ограничительную подсистему.
В sldvdemo_sbr_verification_fixed модель, чтобы запустить анализ, дважды кликает блок Run.
Анализ доказывает валидность свойства.

Документация