В этом примере показов, как доказать свойства в круиз- алгоритм управления с фиксированной точкой. Он ссылается на модель проекта с помощью модели-ссылки так, чтобы исходная модель проекта не изменилась. Правило замены блоков задает свойство, которое проверяет, возможно ли переполнение. Подсистема верификации задает предположение о области значений скорости, вводимой во время проверки свойства. Эта модель конфигурирует Simulink Design Verifier, чтобы применить замену блока к блоку Sum, который питает выход ПИ-контроллера с фиксированной точкой в модели-ссылке и возвращает контрпример, который демонстрирует переполнение.
open_system('sldvdemo_cruise_control_fxp_verification');
