Анализ модели системы управления на соответствие требованиям, смоделированным как свойства, и изучение нарушений свойств с помощью анализа зависимостей.

Поиск нарушения свойств с помощью анализа проверки свойств Simulink ® Design Verifier™. Требования безопасности моделируются в качестве свойств, а затем проверяется соответствие конструкторской модели требованиям.

Проверьте свойства безопасности в модели конструкции реверсивного устройства. Находящийся под ним блок свойств содержит четыре свойства безопасности. Simulink Design Verifier анализирует модель конструкции и свойства безопасности, чтобы доказать правильность или определить контрпримеры. Использование ссылки на модель исключает необходимость добавления проверочного содержимого к конструкторской модели, позволяя проверочному содержимому существовать независимо от конструкции.

Выполните анализ проверки свойств с несколькими свойствами. Модель конфигурируется для анализа, чтобы попытаться доказать, что:

Докажи свойства в алгоритме круиз-контроля с фиксированной точкой. Она ссылается на конструкторскую модель, используя ссылку на модель, так что исходная конструкторская модель остается неизменной. Правило замены блоков определяет свойство, которое проверяет, возможно ли переполнение. Подсистема проверки определяет предположение о диапазоне скорости, вводимой во время проверки свойств. Эта модель настраивает Simulink Design Verifier для применения замены блока к блоку Sum, который подает выходной порт PI-контроллера с фиксированной точкой в ссылочной модели, и возвращает контрпример, демонстрирующий переполнение.

Используйте модель спецификации для выполнения тестирования на основе требований. В этом примере используется систематический подход для проверки проектной модели на соответствие требованиям. Подробное описание модели спецификации см. в разделе Что такое модель спецификации?.