Обзор

В этом примере вы анализируете свойства модели, которые основаны на четырех требованиях системы реверсивного устройства двигателя. Сфальсифицированные результаты анализа свойств позволяют предположить, что требования разработки системы являются неполными - система допускает поведение, которое нарушает несколько из следующих требований:

Чтобы лучше изучить поведение модели, вы анализируете зависимости для входов временных рядов, которые вызывают нежелательное поведение модели, потому что системе не хватает необходимой логики управления. Затем вы анализируете пересмотренную системную модель управления, которая проходит анализ свойств.

Анализ свойств безопасности

1. Нажмите кнопку Открыть модель, чтобы открыть исходную модель и создать рабочую директорию файлов примера.

Подсистема свойств безопасности является блоком Подсистемы верификации из библиотеки Verifier™ Simulink ® Design. Логика верификации в Свойства моделирует требования безопасности. Для примера требование воздушной скорости проверяется:

Дополнительные сведения о блоках Подсистемы верификации см. в разделе Подсистема верификации (Simulink Design Verifier).

2. Просмотрите требования. В модели щелкните значок Показать представления (Show Perspectives) в правом нижнем углу и выберите Требования (Requirements). Откроется панель Requirements (Requirements). Разверните thrust_reverser_safety_requirements.

Требования безопасности связаны с блоками Assertion в Подсистеме свойств безопасности. Блоки Assertion считаются целями доказательства. Статус верификации для каждого требования отражает результаты анализа свойств соответствующего блока Assertion.

3. Просмотр статуса верификации потребностей. Щелкните правой кнопкой мыши одно из требований в браузере и выберите Статус верификации. Столбец «Проверенный» указывает, что требования не выполняются.

4. Анализ свойств модели. На вкладке Приложения нажмите Design Verifier. На вкладке Design Verifier нажмите «Доказать свойства».

Когда анализ свойств завершится, нажмите кнопку Обновить, чтобы обновить статус в столбце Проверено. Результаты показывают, что три из четырех целей сфальсифицированы - анализ обнаружил сигнальное условие, которое фальсифицирует свойства и, следовательно, нарушает требования.

Анализируйте поведение модели с помощью контрпримеров

В окне Проекта Verifier Results Сводных данных нажмите HTML, чтобы открыть детальный анализ отчет. В главе 4 каждое сфальсифицированное свойство перечисляет контрпример. Например, в контрпримере, который фальсифицирует требование воздушной скорости:

Контрпримерные временные ряды указывают на условие, с которым может быть трудно столкнуться в симуляции, но, тем не менее, вызывает поведение модели, которое нарушает требование. Исследуйте поведение путем анализа зависимостей сигнала в контрпримере:

1. На вкладке Design Verifier нажмите кнопку Highlight in Model.

2. Выберите блок допустимых значений скорости в подсистеме Test Модуля > Safety Свойств > airspeed свойства.

3. На вкладке Design Verifier нажмите кнопку Debug Using Slicer. Модель подсвечивает зависимости допустимого значения скорости полета и отображает значения сигналов в T = 0,2.

4. Перейдите на один уровень в модели, в Подсистему свойств безопасности. Шаг назад через время симуляции контрпримера. На вкладке Simulation нажмите Step Back.

5. При T = 0,1 средняя воздушная скорость ниже порога и разворачивается реверсивный двигатель. Продвигаясь вперед, при T = 0,2 средняя воздушная скорость выше порога, и реверс тяги все еще развернут. Это нарушает требование.

Сфальсифицированное свойство и анализ зависимостей предполагают, что алгоритм системы управления не полностью спроектирован, а требования являются неполными.

Анализ переработанной системы

Переработка системы управления требует переосмысления требований. В этом случае отсутствие промежуточного состояния ожидания позволяет нежелательное поведение системы, когда входы изменяются внезапно. Добавление промежуточного режима развертывания, который задерживает ответ реверсивного устройства, решает проблему.

Откройте reqs_validation_property_proving_redesigned_model модель. Откройте thrustReversers график.

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

Создайте ссылки из блоков верификации в переработанной модели к требованиям:

1. В модели на вкладке Приложения щелкните Диспетчер требований.

2. На вкладке Требования щелкните Редактор требований.

3. Откройте thrust_reverser_safety_requirements в редакторе требований.

4. Для требования 1.1, Условие воздушной скорости, ссылка на допустимый блок воздушной скорости в Подсистеме «Свойства безопасности > Свойство воздушной скорости». Перетащите R1.1 из браузера требований в допустимый блок воздушной скорости в модели.

5. Новая ссылка появится в редакторе требований, на панели «Сведения», в разделе « Ссылках».

6. Удалите ссылку на блок assert в исходной модели. Если исходная модель закрыта, эта ссылка появляется неразрешенным. Рядом со ссылкой щелкните значок Удалить ссылку.

7. Повторите для трех других требований и блоков верификации в переработанной модели.

Запустите анализ свойств на пересмотренной модели. Просмотр результатов на панели Requirements.

Результаты показывают, что свойства действительны.