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