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