Функция цели доказательства для диаграмм Stateflow и блоков MATLAB function
Эта функция не имеет никакого выхода и никакого удара на его функцию порождения ни кроме каких косвенных побочных эффектов оценки 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);
Чтобы сохранить обновленный код, во вкладке Editor, нажимают Save и закрывают редактор.
Чтобы доказать свойства безопасности, в Редакторе Simulink®, выбирают подсистему Safety Properties. На вкладке Design Verifier нажмите Prove Properties.
В качестве альтернативы в Редакторе Simulink, можно щелкнуть правой кнопкой по подсистеме Safety Properties и выбрать Design Verifier> Prove Subsystem Properties.
Вместо того, чтобы использовать sldv.prove функция, можно вставить блок Proof Objective в модель. Используя sldv.prove вместо Proof Objective блок предлагает несколько преимуществ, описанных в том, Что Доказывает Свойство?.
Можно также задать цель доказательства при помощи MATLAB для генерации кода, не используя sldv.prove функция. Используя sldv.prove вместо того, чтобы непосредственно использовать MATLAB для генерации кода избавляет от необходимости к:
Опишите цель при помощи блока Simulink.
Явным образом соедините доказательство выход с блоком Simulink.
Proof Assumption | Proof Objective | sldv.condition | sldv.prove | sldv.test | Test Condition | Test Objective
