Что такое Property Proving?

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

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

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

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

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

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

Доказательные блоки

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

  • Proof Objective - задайте значения сигнала, чтобы доказать

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

Примечание

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

Доказательство функций

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

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

  • sldv.assume - Задает доказательство допущения

Эти функции:

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

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

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

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

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

Примечание

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

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