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