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);

В редакторе сохраните обновленный код.

Чтобы доказать свойства безопасности, в Редакторе Simulink®, выбирают подсистему Safety Properties и выбирают Analysis> Design Verifier> Prove Properties> Selected Subsystem.

Также в Редакторе 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
Поддержка