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