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, можно увидеть блоки и функции, но они не дают результатов.
