Рабочий процесс для доказательства свойств модели

Чтобы доказать свойства вашей модели проекта, используйте следующий рабочий процесс:

  1. Определите цели верификации для своей модели проекта, e.g., на основе ваших технических требований требований.

  2. Оснастите свою модель проекта, чтобы задать предположения доказательства и цели доказательства.

    • Для простых свойств оснастите свою модель с блоками или MATLAB® функции, которые задают цели доказательства.

    • Для свойств уровня системы создайте модель верификации, которая содержит блок Model, который ссылается на модель проекта, и задайте свойства в интерфейсе модели проекта использование тех же вводов и выводов.

  3. Задайте аналитические ограничения с помощью блока Proof Assumption или sldv.assume. Эти ограничения применяются ко всем активированным целям доказательства.

    Примечание

    Предположения доказательства применяются ко всем активированным целям доказательства. Убедитесь, что вы не задаете противоречащих предположений, потому что та сила делает недействительным целый анализ.

  4. Задайте опции то управление как Simulink® Design Verifier™ доказывает свойства вашей модели.

  5. Выполните анализ Simulink Design Verifier и рассмотрите результаты.

Для осуществления, которое демонстрирует этот рабочий процесс, смотрите Prove Properties в Модели.

Похожие темы