Можно использовать Simulink® Design Verifier™, чтобы смоделировать конструктивные требования как свойства и затем доказать свойства в модели. Чтобы проверить, что свойства, сопоставленные с требованиями модели, содержат под всеми возможными входными значениями, используйте анализ доказательства свойства. Если требование перестало работать, Simulink Design Verifier обеспечивает контрпримеры, чтобы отладить отказ.
Этот пример объясняет, как можно смоделировать конструктивные требования как свойства при помощи блока Proof Objective и затем проверить, что свойство для упрощенной модели круиз-контроля, обсужденной в, Анализирует Простую Модель Круиз-контроля.
Модель sldvexSimpleCruiseControlProperties состоит из Подсистемы Верификации, которая состоит из функциональных требований, смоделированных при помощи блока Proof Objective.
load_system('sldvexSimpleCruiseControlProperty'); open_system('sldvexSimpleCruiseControlProperty/Verification Subsystem');
На вкладке Apps кликните по стреле на дальнем правом от раздела Apps. Под Model Verification Валидация и галерея Test, нажимают Design Verifier.
Чтобы выполнить анализ доказательства свойства, нажмите Prove Properties. Программное обеспечение анализирует модель и отображает результаты в окне Results Summary. Результат показывает, что одна цель допустима при приближении.
На вкладке Design Verifier, в разделе Review Results, нажимают Highlight in Model.
Свойство, которое допустимо при приближении, подсвечено в оранжевом. Кликните по блоку Proof Objective. Окно Results Inspector отображает цели блока Proof Objective.
Чтобы просмотреть отчет HTML, в разделе Review Results, нажимают HTML Report. Глава Состояния Цели доказательства перечисляет цель доказательства, которая найдена допустимой при приближении.
