В этом примере показано, как найти нарушение свойства с помощью анализа доказательства свойства Verifier™ Simulink ® Design. Вы моделируете требования безопасности как свойства, а затем проверяете модель проекта на соответствие требованиям.
При выполнении анализа доказательства свойств Simulink Design Verifier генерирует контрпример, который используется для отладки нарушения свойства.
The 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 нажмите «Доказать свойства».
После завершения анализа окно Сводных данных результатов сообщает, что одна цель была сфальсифицирована.
Создается модель тестовой обвязки, и открывается диалоговое окно Signal Builder, в котором отображается контрпример.
В диалоговом окне Signal Builder нажмите кнопку Start ▸.
В окне Diagnostic Viewer отображается ошибка, указывающая, что симуляция была завершена, поскольку в это время произошла проверка типа «assertion» 0.04.
Вы также можете отлаживать нарушение свойства с помощью Model Slicer. Для получения дополнительной информации смотрите Отладку Свойства Доказывание нарушений при помощи Slicer модели.
Ошибочное поведение, проявляемое в примере счетчика, фиксируется в sldvdemo_cruise_control_verification_fixed модель.
open_system('sldvdemo_cruise_control_verification_fixed');
В рабочем процессе проверки свойств может потребоваться перепроектировать систему и/или переопределить свойство и выполнить такие итерации.
Откройте ссылочную модель sldvdemo_cruise_control_fixed и откройте Controller подсистема. В этой подсистеме обновленная модель проекта сбрасывает выход дросселя, когда Активно Управление.
На вкладке Design Verifier нажмите «Доказать свойства». После завершения анализа окно Сводных данных результатов сообщает, что цель действительна.