Exponenta Banner

sldv.prove

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

свернуть все на странице

Синтаксис

sldv.prove(expr)

Описание

пример

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

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

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

свернуть все

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

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

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

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

  • Опишите цель при помощи блока Simulink.

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

Смотрите также

| | | | | |

Темы

Представленный в R2009b

Документация Simulink Design Verifier

Поддержка