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