Шаг 1: откройте модель

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');

Шаг 2: выполните анализ доказательства свойства

На вкладке Design Verifier нажмите Prove Properties.

После того, как анализ завершается, окно Results Summary сообщает, что одна цель была сфальсифицирована.

Модель тестовой обвязки сгенерирована, и диалоговое окно Signal Builder открывает и отображается контрпример.

Шаг 3: симулируйте контрпример, чтобы реплицировать ошибку

В диалоговом окне Signal Builder нажмите кнопку симуляции Start ▸.

Окно Diagnostic Viewer отображает ошибку при утверждении, что симуляция была отключена, потому что утверждение произошло во время 0.04.

Опционально, можно отладить нарушение свойства при помощи Ножа Модели. Для получения дополнительной информации смотрите Свойство Отладки Доказать Нарушения при помощи Ножа Модели.

Шаг 4: откройте фиксированную модель

Ошибочное поведение, предоставленное встречным примером, фиксируется в sldvdemo_cruise_control_verification_fixed модель.

open_system('sldvdemo_cruise_control_verification_fixed');

В рабочем процессе доказательства свойства можно быть обязаны перепроектировать систему и/или переопределять свойство и выполнять такие итерации.

Откройте модель sldvdemo_cruise_control_fixed, на которую ссылаются, и откройте Controller подсистема. В этой подсистеме обновленная модель проекта сбрасывает дроссель выход, когда Активное Управление активно.

На вкладке Design Verifier нажмите Prove Properties. После того, как анализ завершается, окно Results Summary сообщает, что цель допустима.

Смотрите также