Целевая функция проверки для диаграмм статофлоу и функциональных блоков MATLAB
Эта функция не имеет выхода и не влияет на ее родительскую функцию, кроме каких-либо косвенных побочных эффектов оценки expr. При выполнении этой функции из командной строки MATLAB ® эта функция не действует.
Вкрапить sldv.prove подтверждение допущений в коде или разделение допущений на сценарий проверки.
Укажите цель доказательства свойства и допущение доказательства в sldvdemo_sqrt_blockrep с использованием функционального блока MATLAB.
Откройте окно sldvdemo_sbr_verification модель и сохраните ее как ex_sldvdemo_sbr_verification.
Откройте подсистему свойств безопасности.
Откройте блок свойств MATLAB, который является блоком функций MATLAB.
В конце check_reminder определение функции, добавление sldv.assume(Inputs.KEY==0 | 1); чтобы последние две строки определения функции были:
sldv.prove(implies(activeCond, SeatBeltIcon)); sldv.assume(Inputs.KEY==0 | 1);
Чтобы сохранить обновленный код, на вкладке «Редактор» нажмите кнопку «Сохранить» и закройте редактор.
Для подтверждения свойств безопасности в редакторе Simulink ® выберите подсистему свойств безопасности. На вкладке Design Verifier щелкните Доказать свойства .
Либо в редакторе Simulink можно щелкнуть правой кнопкой мыши подсистему свойств безопасности и выбрать Design Verifier > Доказать свойства подсистемы.
Вместо использования sldv.prove можно вставить блок Proof Objective в модель. Используя sldv.prove вместо блока Proof Objective предлагает несколько преимуществ, описанных в документе What Is Property Proving?.
Можно также указать цель подтверждения с помощью MATLAB для создания кода без использования sldv.prove функция. Используя sldv.prove вместо непосредственного использования MATLAB для генерации кода устраняет необходимость:
Выражайте цель с помощью блока Simulink.
Явное подключение выходного сигнала проверки к блоку Simulink.
Допущение доказательства | Цель доказательства | sldv.condition | sldv.prove | sldv.test | Условие испытания | Цель тестирования