Свойство - это требование, которое моделируется в Simulink ® или Stateflow ® или с использованием функциональных блоков MATLAB. Свойство может быть простым требованием, например сигналом в модели, который должен достигать определенного значения или диапазона значений во время моделирования.
Свойство также может быть требованием в модели, которое включает в себя ряд входных и выходных сигналов, смоделированных как логическое выражение, которое необходимо доказать.
Программа Simulink Design Verifier™ выполняет формальный анализ модели, чтобы доказать или опровергнуть указанные свойства. После завершения анализа программное обеспечение предлагает несколько способов просмотра результатов:
Выделено на модели
Модель кабельных трасс с тестовыми примерами
Подробный отчет в формате HTML
Программа Simulink Design Verifier предоставляет два блока, чтобы можно было указать доказательства свойств в моделях Simulink:
Цель доказательства - определение значений сигнала для подтверждения
Предположение о подтверждении - ограничение значений сигнала во время подтверждения
Примечание
Блоки из библиотеки проверки модели в программном обеспечении Simulink ведут себя подобно блокам Proof Objective во время проверки доказательств Simulink Design Verifier. Для задания свойств модели можно использовать блоки утверждения и другие блоки проверки модели. Дополнительные сведения об этих блоках см. в разделе Проверка модели.
Программное обеспечение Simulink Design Verifier предоставляет две функции создания кода Stateflow и MATLAB ® для проверки свойств модели Simulink или диаграммы Stateflow:
sldv.prove - Указывает цель подтверждения
sldv.assume - Указывает предположение доказательства
Эти функции:
Определение математических отношений для проверки свойств в форме, которая может быть более естественной, чем использование параметров блока
Поддержка задания нескольких целей, допущений или условий без усложнения модели.
Обеспечение доступа к питанию MATLAB.
Поддержка разделения проверки и проектирования модели.
Пример использования этих функций подтверждения см. в разделе sldv.prove справочная страница.
Примечание
Блоки и функции Simulink Design Verifier сохраняются вместе с моделью. При открытии модели в установке MATLAB, не имеющей лицензии Simulink Design Verifier, можно просмотреть блоки и функции, но они не дают результатов.