sldv.prove

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

Синтаксис

Описание

пример

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

Эта функция не имеет выхода и никакого влияния на ее родительскую функцию, кроме любых косвенных побочных эффектов оценки expr. Если вы выпускаете эту функцию из MATLAB® командная строка, функция не имеет эффекта.

Интерсперсные sldv.prove доказательство допущений в коде или разделение допущений на скрипты верификации.

Примеры

свернуть все

Задайте цель доказательства свойства и доказательство допущения в sldvdemo_sqrt_blockrep моделировать при помощи блока MATLAB Function.

Откройте sldvdemo_sbr_verification моделировать и сохранить как ex_sldvdemo_sbr_verification.

Откройте подсистему Свойства.

Откройте блок 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® Редактор, выберите Подсистему свойств безопасности. На вкладке Design Verifier нажмите Prove Properties.

Кроме того, в редакторе Simulink можно щелкнуть правой кнопкой мыши Подсистему свойств безопасности и выбрать Design Verifier > Prove Subsystem Properties.

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

свернуть все

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

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

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

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

  • Выразите цель при помощи блока Simulink.

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

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