В этом примере показано, как отладить нарушения доказательства свойства при помощи Ножа Модели. Рассмотрите модель sldvdemo_cruise_control_verification. Эта модель содержит блок Assertion.
Модели Safety Properties подсистемы Верификации свойство, которое должно сохраняться для модели проекта. Эта подсистема содержит Блок Утверждения (BrakeAssertion), который проверяет свойство. Анализ Доказательства Свойства Simulink Design Verifier попытается сфальсифицировать утверждение. Если Simulink Design Verifier будет успешен, то он сгенерирует контрпример, фальсифицирующий утверждение. Мы можем использовать Нож Модели, чтобы отладить это сфальсифицированное утверждение.
1. Открытая модель sldvdemo_cruise_control_verification.
open_system ('sldvdemo_cruise_control_verification')
2. Откройте Simulink Design Verifier путем нажатия на Apps> Design Verifier.
3. Нажмите Prove Properties. Simulink Design Verifier анализирует модель и отображает результаты в окне Results Summary.
Модель подсвечивает подсистему, где блок Assertion расположен.
4. Подсистема Open Safety Properties и выбор сфальсифицированный блок Assertion.
5. Нажмите Debug Using Slicer в меню панели инструментов, чтобы отладить Нож Модели использования нарушения. В качестве альтернативы можно нажать Debug в окне Inspector результатов.
При Нажатии на любую из точек входа следующая настройка сделана на модели:
a. The Assertion block is added as a starting point for Model Slicer. b. The model is highlighted with the counterexample generated by Simulink Design Verifier analysis. c. The design model is simulated and paused at the time-step of assertion failure.
6. Отладьте и анализируйте модель при помощи кнопок Step Back и Step Forward и осмотр Меток порта.
Утверждать стендовые испытания двигателя, если выход A подразумевает B (==> B) является ложным.
A верен, когда вход тормоза в верен для трех последовательных временных шагов.
B верен когда Throttle_out <= 0
Можно заметить, что симуляция останавливается в t=0.04, когда условие ==> B является ложным. Это может наблюдаться от Меток порта.
a. На вкладке Simulation нажмите Step Back, чтобы видеть метки порта всех блоков в T = (T-0.1).
Можно заметить, что Метка порта A является ложной до T=0.04, когда это становится верным. В этой точке Метка порта B является ложной (Throttle_Out> 0). Свойство сфальсифицировано, потому что Throttle_Out больше 0.
b. Чтобы просмотреть блоки, который приводит к отказу, откройте Модель проекта> Контроллер. Зависимые блоки и путь подсвечены.
Чтобы просмотреть фиксацию, откройте sldvdemo_cruise_control_verification модель и нажатие кнопки кнопка Open Fixed Model на холсте.