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