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