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