Если ваша модель имеет свойства в масштабе всей системы, которые влияют на поведение модели, вы можете хотеть доказать свойства, не изменяя модель проекта. Для этого вы создаете verification model, который включает:
Блок Model это ссылается на модель проекта
Одна или несколько подсистем верификации, которые задают свойства и любые необходимые ограничения
Модели sldvdemo_sbr_design модели проекта логика для света напоминания о ремне безопасности. Если воспламенение включено, ремни безопасности откреплены, и автомобиль превышает определенную скорость, свет напоминания о ремне безопасности включает.
Модель sldvdemo_sbr_verification является моделью верификации, которая задает некоторые ограничения и проверяет свойства в модели sldvdemo_sbr_design. Блок Model в моделях - ссылках верификации модель проекта, так, чтобы логика верификации существовала только в модели верификации.
Модель sldvdemo_sbr_verification содержит свойство, которое сфальсифицировано, потому что ограничение отключено. В модели sldvdemo_sbl_verification_fixed включено ограничение, и все свойства доказаны допустимыми.
Сделайте эти шаги, чтобы понять, как модель верификации работает:
Откройте модель верификации:
Блок 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.
Анализ доказывает валидность свойства.
