Чтобы доказать свойства вашей модели проекта, используйте следующий рабочий процесс:
Определите цели верификации для вашей модели проекта, например, на основе ваших спецификаций требований.
Измерьте свою модель проекта, чтобы задать цели доказательства и доказательные допущения.
Для простых свойств инструментируйте свою модель блоками или MATLAB® функции, которые определяют цели доказательства.
Для свойств уровня системы создайте модель верификации, которая содержит блок Model, который ссылается на модель проекта, и определите свойства интерфейса модели проекта с помощью тех же входных и выходных параметров.
Определите ограничения анализа с помощью блока или sldv.assume Proof Assumption. Эти ограничения применяются ко всем включенным целям доказательства.
Примечание
Доказанные допущения применяются ко всем включенным целям доказательства. Убедитесь, что вы не задаете никаких противоречивых допущений, потому что это может сделать недействительным весь анализ.
Задайте опции, которые управляют тем, как Simulink® Design Verifier™ доказывает свойства вашей модели.
Выполните анализ Simulink Design Verifier и проверьте результаты.
Для упражнения, которое демонстрирует этот рабочий процесс, смотрите Доказательство свойств в модели.
