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

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

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

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

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

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

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

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

Осмыслите модель верификации

Выполните следующие шаги, чтобы понять, как работает модель верификации:

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

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

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

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

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

Исправьте модель верификации

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

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

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

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