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).
Программное обеспечение Simulink Design Verifier предоставляет два Stateflow и MATLAB® для функций генерации кода, чтобы задать свойство, доказывающее для модели Simulink или диаграммы Stateflow:
sldv.prove — Задает цель доказательства
sldv.assume — Задает предположение доказательства
Эти функции:
Идентифицируйте математические отношения для доказательства свойств в форме, которая может быть более естественной, чем использование параметров блоков
Поддержка, задающая несколько целей, предположений или условий, не усложняя модель.
Обеспечьте доступ к степени MATLAB.
Поддержите разделение верификации и проекта модели.
Для примера того, как использовать эти функции доказательства, смотрите sldv.prove страница с описанием.
Блоки Simulink Design Verifier и функции сохранены с моделью. Если вы открываете модель на установке MATLAB, которая не имеет лицензии Simulink Design Verifier, вы видите блоки и функции, но они не приводят к результатам.
