Что доказывает свойство?

property является требованием, чтобы вы смоделировали в Simulink® или Stateflow® или использовании блоки MATLAB Function. Свойство может быть простым требованием, таким как сигнал в вашей модели, которая должна достигнуть особого значения или области значений значений в процессе моделирования.

Свойство может также быть требованием к модели, которая включает много сигналов ввода и вывода, смоделированных как логическое выражение, которое должно быть доказано.

Программное обеспечение Simulink Design Verifier™ выполняет формальный анализ вашей модели, чтобы доказать или опровергнуть заданные свойства. После завершения анализа программное обеспечение предлагает несколько способов для вас рассмотреть результаты:

  • Подсвеченный на модели

  • Модель тестовой обвязки с тестами

  • Подробный отчет HTML

Блоки доказательства

Программное обеспечение Simulink Design Verifier обеспечивает два блока, таким образом, можно задать доказательства свойства в моделях Simulink:

  • Proof Objective — Задайте значения сигнала доказать

  • Proof Assumption — Ограничьте значения сигнала во время доказательства

Примечание

Блоки из библиотеки Model Verification в программном обеспечении Simulink ведут себя как блоки Цели доказательства во время доказательств Simulink Design Verifier. Можно использовать блоки Assertion и другие блоки Model Verification, чтобы задать свойства модели. Для получения дополнительной информации об этих блоках, смотрите Model Verification.

Функции доказательства

Программное обеспечение Simulink Design Verifier предоставляет два Stateflow и MATLAB® для функций генерации кода, чтобы задать свойство, доказывающее для модели Simulink или диаграммы Stateflow:

  • sldv.prove — Задает цель доказательства

  • sldv.assume — Задает предположение доказательства

Эти функции:

  • Идентифицируйте математические отношения для доказательства свойств в форме, которая может быть более естественной, чем использование параметров блоков

  • Поддержка, задающая несколько целей, предположений или условий, не усложняя модель.

  • Обеспечьте доступ к степени MATLAB.

  • Поддержите разделение верификации и проекта модели.

Для примера того, как использовать эти функции доказательства, смотрите sldv.prove страница с описанием.

Примечание

Блоки Simulink Design Verifier и функции сохранены с моделью. Если вы открываете модель на установке MATLAB, которая не имеет лицензии Simulink Design Verifier, вы видите блоки и функции, но они не приводят к результатам.

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