В этом примере показано, как найти нарушение свойства при помощи анализа доказательства свойства Simulink® Design Verifier™. Вы моделируете требования техники безопасности как свойства и затем проверяете модель проекта по требованиям.
Когда вы выполняете анализ доказательства свойства, Simulink Design Verifier генерирует контрпример, который вы используете, чтобы отладить нарушение свойства.
sldvdemo_cruise_control_verification модель содержит модель - ссылку к sldvdemo_cruise_control_defective модель проекта. Модель проекта является системой круиз-контроля, которая состоит из ПИ-контроллера, который вычисляет дроссель выход на основе различия между фактической и целевой скоростью.
open_system('sldvdemo_cruise_control_verification');
Свойства безопасности для дросселя выход моделируются в Safety Properties подсистема верификации блоком Assertion.
open_system('sldvdemo_cruise_control_verification/Safety Properties');
На вкладке Design Verifier нажмите Prove Properties.
После того, как анализ завершается, окно Results Summary сообщает, что одна цель была сфальсифицирована.
Модель тестовой обвязки сгенерирована, и диалоговое окно Signal Builder открывает и отображается контрпример.
В диалоговом окне Signal Builder нажмите кнопку симуляции Start ▸.
Окно Diagnostic Viewer отображает ошибку при утверждении, что симуляция была отключена, потому что утверждение произошло во время 0.04.
Опционально, можно отладить нарушение свойства при помощи Ножа Модели. Для получения дополнительной информации смотрите Свойство Отладки Доказать Нарушения при помощи Ножа Модели.
errorneous поведение, предоставленное встречным примером, фиксируется в sldvdemo_cruise_control_verification_fixed модель.
open_system('sldvdemo_cruise_control_verification_fixed');
В рабочем процессе доказательства свойства можно потребовать, чтобы перепроектировать систему и/или переопределить свойство и выполнить такие итерации.
Откройте модель sldvdemo_cruise_control_fixed, на которую ссылаются, и откройте Controller подсистема. В этой подсистеме обновленная модель проекта сбрасывает дроссель выход, когда Активное Управление активно.
На вкладке Design Verifier нажмите Prove Properties. После того, как анализ завершается, окно Results Summary сообщает, что цель допустима.