В этом примере показано, как отлаживать свойства, доказывающие нарушения, с помощью модели Slicer. Рассмотрим модель sldvdemo_cruise_control_verification. Эта модель содержит блок утверждения.
Подсистема проверки «Свойства безопасности» моделирует свойство, которое должно иметь значение true для модели конструкции. Эта подсистема содержит блок утверждения (Assertion), который проверяет свойство. Анализ проверки свойств Simulink Design Verifier попытается сфальсифицировать утверждение. Если Simulink Design Verifier успешно работает, это приведет к созданию контрпримера, фальсифицирующего утверждение. Мы можем использовать модель Slicer для отладки этого фальсифицированного утверждения.
1. Открыть sldvdemo_cruise_control_verification модели.
open_system ('sldvdemo_cruise_control_verification')
2. Откройте Simulink Design Verifier, щелкнув Приложения > Design Verifier.
3. Щелкните Доказать свойства. Simulink Design Verifier анализирует модель и отображает результаты в окне Сводка результатов (Results Summary).
Модель выделяет подсистему, в которой расположен блок утверждения.
4. Откройте подсистему свойств безопасности и выберите фальсифицированный блок утверждения.
5. Щелкните Отладка с помощью среза (Debug Using Slicer) в меню панели инструментов, чтобы отладить нарушение с помощью среза модели. Можно также щелкнуть Отладка (Debug) в окне Инспектор результатов (results Inspector).
При щелчке любой из точек входа в модели выполняется следующая настройка:
a. Блок Assertion добавляется в качестве начальной точки для модели Slicer.
b. Модель подсвечивается контрпримером, сгенерированным анализом Simulink Design Verifier.
с. Конструкторская модель моделируется и приостанавливается на этапе неуспешного утверждения.
6. Выполните отладку и анализ модели с помощью кнопок Шаг назад (Step Back) и Шаг вперед (Step Forward) и проверьте метки порта.
Блок Assert проверяет, имеет ли выход A значение B (A = = > B) значение false.
А является истинным, когда вход тормоза в является истинным в течение трех последовательных временных шагов.
B имеет значение true, если Throttle_out < = 0
Можно заметить, что моделирование останавливается при t = 0,04, когда условие A = = > B является ложным. Это можно увидеть на этикетках портов.
О. На вкладке Simulation (Моделирование) нажмите кнопку Step Back (Шаг назад), чтобы увидеть метки портов всех блоков в T = (T-0.1).
Можно заметить, что метка порта A имеет значение false до T = 0.04, когда она станет истинной. На этом этапе метка порта B имеет значение false (Throttle_Out > 0). Свойство сфальсифицировано, так как Throttle_Out больше 0.
b. Чтобы просмотреть блоки, приводящие к сбою, откройте меню «Модель конструкции» > «Контроллер». Зависимые блоки и контур подсвечиваются.
Чтобы просмотреть исправление, откройте sldvdemo_cruise_control_verification и нажмите кнопку Открыть фиксированную модель (Open Fixed Model) на холсте.