sldv.assume

Предположение доказательства функционирует для диаграмм Stateflow и блоков MATLAB function

Синтаксис

Описание

пример

sldv.assume(expr) задает тот expr верно для каждой оценки при доказательстве свойств. Используйте любое допустимое Булево выражение для expr.

Эта функция не имеет никакого выхода и никакого удара на его функцию порождения ни кроме каких косвенных побочных эффектов оценки 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.

Входные параметры

свернуть все

Выражение MATLAB, например, x > 0.

Альтернативы

Вместо того, чтобы использовать sldv.assume функция, можно вставить блок Proof Assumption в модель. Используя sldv.assume вместо Proof Assumption блок предлагает несколько преимуществ, описанных в том, Что Доказывает Свойство?.

При доказательстве моделей при помощи MATLAB для генерации кода можно также ограничить значения сигналов, не используя sldv.assume функция. Используя sldv.assume вместо того, чтобы непосредственно использовать MATLAB для генерации кода избавляет от необходимости к:

  • Опишите предположение при помощи блока Simulink.

  • Явным образом соедините предположение выход с блоком Simulink.

Представленный в R2009b
Для просмотра документации необходимо авторизоваться на сайте