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