Предположение доказательства функционирует для диаграмм Stateflow и блоков MATLAB function
Эта функция не имеет никакого выхода и никакого удара на его функцию порождения ни кроме каких косвенных побочных эффектов оценки expr. Если вы выпускаете эту функцию из командной строки MATLAB®, функция не оказывает влияния.
Вкрапите sldv.assume предположения доказательства в рамках кода MATLAB или разделяют предположения на скрипт верификации.
Опция Proof assumptions в панели Property proving применяется к предположениям доказательства, представленным sldv.assume функционируйте и блоком Proof Assumption.
Задайте цель доказательства свойства и предположение доказательства в sldvdemo_sbr_verification модель при помощи блока 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.assume функция, можно вставить блок Proof Assumption в модель. Используя sldv.assume вместо Proof Assumption блок предлагает несколько преимуществ, описанных в том, Что Доказывает Свойство?.
При доказательстве моделей при помощи MATLAB для генерации кода можно также ограничить значения сигналов, не используя sldv.assume функция. Используя sldv.assume вместо того, чтобы непосредственно использовать MATLAB для генерации кода избавляет от необходимости к:
Опишите предположение при помощи блока Simulink.
Явным образом соедините предположение выход с блоком Simulink.
Proof Assumption | Proof Objective | sldv.condition | sldv.prove | sldv.test | Test Condition | Test Objective
