Функция цели доказательства для диаграмм 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 | Test Condition | Test Objective | sldv.condition | sldv.prove | sldv.test
