Подтвердите требование, установленное путем анализа свойств та модель отдельные требования. Сфальсифицированные свойства указывают на проект и неполноту набора требования.
В этом примере вы анализируете свойства модели, которые основаны на четырех требованиях системы инвертора тяги механизма. Сфальсифицированные результаты анализа свойства предполагают, что требования разработки системы являются неполными - система позволяет поведение, которое нарушает несколько из следующих требований:
Инвертор тяги не должен развертываться, если скорость полета будет больше 150 узлов.
Инвертор тяги не должен развертываться, если самолет будет в воздухе, как обозначено значением веса на датчиках колес. Если самолет находится в воздухе, значением сигналов для каждого из двух датчиков веса на колесах (WOW) является false.
Инвертор тяги не должен развертываться, если значение любого датчика тяги будет положительно.
Инвертор тяги не должен развертываться, если скорость вращения колес посадочного устройства будет меньше порогового значения.
Чтобы лучше изучить поведение модели, вы анализируете зависимости какое-то время серийный вход, который вызывает нежелательное поведение модели, потому что система испытывает недостаток в требуемой управляющей логике. Затем вы анализируете пересмотренную модель системы управления, которая передает анализ свойства.
1. Нажмите кнопку Open Model, чтобы открыть исходную модель и создать рабочую директорию файлов в качестве примера.
Подсистема Safety Properties является блоком Subsystem Верификации от библиотеки Simulink® Design Verifier™. Логика верификации в моделях Safety Properties требования техники безопасности. Например, требование скорости полета проверяется:
Для получения дополнительной информации о блоках Subsystem Верификации, смотрите Подсистему Верификации.
2. Просмотрите требования. В модели щелкните, Перспективы Показа просматривает значок в нижнем правом углу, и выберите Requirements. Панель Requirements открывается. Расширьте thrust_reverser_safety_requirements.
Требования техники безопасности соединяются с блоками Утверждения в подсистеме Safety Properties. Блоки Утверждения рассматриваются целями доказательства. Состояние верификации для каждого требования отражает результаты анализа свойства своего соответствующего блока Assertion.
3. Отобразите состояние верификации для требований. Щелкните правой кнопкой по одному из требований в браузере и выберите Verification Status. Проверенный столбец указывает, что требования не выполняются.
4. Анализируйте свойства модели. Во вкладке Apps нажмите Design Verifier. Во вкладке Design Verifier нажмите Prove Properties.
Когда анализ свойства завершится, нажмите Кнопку Обновить, чтобы обновить состояние в Проверенном столбце. Результаты показывают, что три из четырех целей сфальсифицированы - анализ нашел условие сигнала, которое фальсифицирует свойства, и поэтому нарушает требования.
Из окна Design Verifier Results Summary нажмите HTML, чтобы открыть отчет детального анализа. В Главе 4, каждый сфальсифицированные списки свойств контрпример. Например, в контрпримере, который фальсифицирует требование скорости полета:
В t = 0.1, инвертор тяги развертывается со скоростью полета ниже порога.
В t = 0.2, инвертор тяги все еще развертывается со скоростью полета выше порога.
Временные ряды контрпримера указывают на условие, которое может затруднить, чтобы столкнуться в симуляции, но тем не менее вызывает поведение модели, которое нарушает требование. Исследуйте поведение путем анализа зависимостей сигнала в контрпримере:
1. Во вкладке Design Verifier нажмите кнопку Highlight in Model.
2. Выберите скорость полета допустимый блок утверждения в Тестовом Модуле> Safety Properties> подсистема свойства скорости полета.
3. Во вкладке Design Verifier нажмите кнопку Debug Using Slicer. Модель подсвечивает зависимости скорости полета допустимое утверждение и отображает значения сигналов в T = 0.2.
4. Переместите один уровень вверх в модели к подсистеме Safety Properties. Отступите через время симуляции контрпримера. Во вкладке Simulation нажмите Step Back.
5. В T = 0.1, средняя скорость полета ниже порога, и инвертор тяги развертывается. Выходить вперед, в T = 0.2, средняя скорость полета выше порога, и инвертор тяги все еще развертывается. Это нарушает требование.
Сфальсифицированное свойство и анализ зависимостей предполагают, что алгоритм системы управления не полностью спроектирован, и требования являются неполными.
Перепроектирование системы управления требует заново обдумавших требований. В этом случае отсутствие промежуточного резервного состояния позволяет нежелательное поведение системы, когда входные параметры внезапно изменяются. Добавление промежуточного режима развертывания, который задерживает ответ инвертора тяги, решает вопрос.
Откройте reqs_validation_property_proving_redesigned_model модель. Откройте thrustReversers график.
Дополнительные конструктивные требования утверждают, что инвертор тяги должен развернуться после паузы. Перепроектированная модель включает:
Дополнительный aboutToBeDeployed состояние.
Расширенные условия перехода, которые возвращаются к undeployed.
Создайте ссылки из блоков верификации в перепроектированной модели к требованиям:
1. В модели, от вкладки Apps, нажимают Requirements Manager.
2. Во вкладке Requirements нажмите Requirements Editor.
3. Открытый thrust_reverser_safety_requirements в редакторе требований.
4. Для требования 1.1, Условия Скорости полета, ссылки на скорость полета допустимый блок в Safety Properties> подсистема свойства скорости полета. Перетащите R1.1 от браузера требований до скорости полета допустимый блок в модели.
5. Новая ссылка появляется в редакторе Линксе Требований панель.
6. Удалите ссылку на утверждать блок в исходной модели. Если исходная модель закрывается, эта ссылка кажется неразрешенной. Рядом со ссылкой кликните по Удалить значку Ссылки.
7. Повторитесь для других трех требований и блоков верификации в перепроектированной модели.
Запустите анализ свойства пересмотренной модели. Просмотрите результаты в Панели Requirements.
Результаты показывают, что свойства допустимы.
