Если модель имеет общесистемные свойства, влияющие на поведение модели, может потребоваться подтверждение свойств без изменения конструкторской модели. Для этого создается модель проверки, которая включает в себя:
Блок модели, который ссылается на модель конструкции
Одна или несколько подсистем проверки, которые определяют свойства и любые требуемые ограничения
Модель конструкции sldvdemo_sbr_design моделирует логику для сигнала напоминания ремня безопасности. Если зажигание включено, ремни безопасности расстегиваются, а машина превышает определенную скорость, включается свет напоминания ремня безопасности.
sldvdemo_sbr_verification модель является моделью проверки, которая определяет некоторые ограничения и проверяет свойства в sldvdemo_sbr_design модель. Блок Модель (Model) в модели проверки ссылается на модель конструкции, так что логика проверки существует только в модели проверки.
sldvdemo_sbr_verification модель содержит фальсифицированное свойство, поскольку ограничение отключено. В sldvdemo_sbl_verification_fixed модель, ограничение включено, и все свойства доказаны.
Выполните следующие шаги, чтобы понять, как работает модель проверки:
Откройте модель проверки:
Блок конструкторской модели является блоком модели, который ссылается на sldvdemo_sbr_design. Диаграмма SBR Stateflow ® в конструкторской модели предполагает, что KEY входное значение первоначально равно 0.
Откройте подсистему «Свойства безопасности», определяющую свойства конструкторской модели, которые требуется доказать.
Эта подсистема содержит функциональный блок MATLAB, называемый свойством MATLAB. Код в этом блоке определяет свойство, в соответствии с которым напоминание о ремне безопасности должно включаться при включении зажигания, ремень безопасности не крепится и скорость составляет менее 15:
Закройте подсистему свойств безопасности.
Откройте подсистему ограничений ввода.
Эта подсистема определяет следующие ограничения:
Ключ может иметь три позиции: 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™ показывает, что одна цель сфальсифицирована - требуется моделирование. Дополнительные сведения см. в разделе Сфальсифицированные цели - требуется моделирование.
Чтобы увидеть, какая цель была сфальсифицирована, щелкните Подсветить результаты анализа на модели.
Подсистема свойств безопасности выделена оранжевым цветом.
Откройте подсистему свойств безопасности и щелкните на блоке свойств MATLAB.
Окно Результаты Simulink Design Verifier указывает, что инструкция
sldv.prove(implies(activeCond,SeatBeltIcon))
было ложным по крайней мере в течение одного временного шага.
Щелкните Просмотр контрпримера, чтобы увидеть значения сигнала, нарушающие это свойство.
Откроется блок Построитель сигналов (Signal Builder) с обратным примером. KEY изначально было 2, что является недопустимым.
Для проверки свойства, указанного в подсистеме свойств безопасности, необходимо убедиться, что начальное значение KEY равно 0.
Подсистема входных ограничений в модели проверки содержала три ограничения. Третье ограничение, которое требует, чтобы начальное значение KEY быть 0, и KEY может изменяться только с шагом 1, отключен.
Чтобы увидеть, как это свойство проверяется при включении третьего ограничения:
В sldvdemo_sbr_verification щелкните Открыть фиксированную модель (Open Fixed Model).
sldvdemo_sbr_verification_fixed откроется модель проверки.
Откройте подсистему ограничений ввода.
Это третье ограничение теперь включено, так что KEY имеет начальное значение 0 и изменяется с шагом 1.
Закройте подсистему ограничений ввода.
В sldvdemo_sbr_verification_fixed для начала анализа дважды щелкните блок Run.
Анализ доказывает действительность имущества.