property является требованием, чтобы вы смоделировали в Simulink® или Stateflow® или блоках MATLAB function использования. Свойство может быть простым требованием, таким как сигнал в вашей модели, которая должна достигнуть особого значения или области значений значений во время симуляции.
Свойство может также быть требованием к модели, которая включает много сигналов ввода и вывода, смоделированных как логическое выражение, которое должно быть доказано.
Программное обеспечение Simulink Design Verifier™ выполняет формальный анализ вашей модели, чтобы доказать или опровергнуть заданные свойства. После завершения анализа программное обеспечение предлагает несколько способов для вас рассмотреть результаты:
Подсвеченный на модели
Модель тестовой обвязки с тестами
Подробный отчет HTML
Программное обеспечение Simulink Design Verifier обеспечивает два блока, таким образом, можно задать доказательства свойства в моделях Simulink:
Цель доказательства — Задает значения сигнала доказать
Предположение доказательства — Ограничивает значения сигнала во время доказательства
Блоки от библиотеки Model Verification в программном обеспечении Simulink ведут себя как блоки Цели доказательства во время доказательств Simulink Design Verifier. Можно использовать блоки Утверждения и другие блоки 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, вы видите блоки и функции, но они не приводят к результатам.
