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

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