Проверка набора требований путем анализа свойств, моделирующих отдельные требования. Фальсифицированные свойства указывают на неполноту проекта и набора требований.
В этом примере анализируются свойства модели, основанные на четырех требованиях к системе реверсивного устройства тяги двигателя. Фальсифицированные результаты анализа свойств позволяют предположить, что требования к конструкции системы являются неполными - система допускает поведение, которое нарушает несколько из следующих требований:
Реверсивное устройство не должно разворачиваться, если скорость воздуха превышает 150 узлов.
Реверсивное устройство не должно разворачиваться, если самолет находится в воздухе, как указано значением веса на датчиках колес. Если самолет находится в воздухе, значение сигнала для каждого из двух датчиков веса на колесах (WOW) составляет false.
Реверсивное устройство не должно развертываться при положительном значении ни одного из датчиков тяги.
Реверсивное устройство не должно развертываться, если скорость вращения колес шасси меньше порогового значения.
Чтобы лучше понять поведение модели, необходимо проанализировать зависимости для входных временных рядов, которые вызывают нежелательное поведение модели, поскольку в системе отсутствует необходимая логика управления. Затем выполняется анализ пересмотренной модели системы управления, которая проходит анализ свойств.
1. Нажмите кнопку Открыть модель (Open Model), чтобы открыть исходную модель и создать рабочую папку файлов примеров.
Подсистема свойств безопасности является блоком подсистемы проверки из библиотеки Simulink ® Design Verifier™. Логика проверки в свойствах безопасности моделирует требования безопасности. Например, требования к скорости воздуха проверяются:
Дополнительные сведения о блоках подсистемы проверки см. в разделе Подсистема проверки.
2. Просмотрите требования. В модели щелкните значок Показать виды (Show Perspectives) в нижнем правом углу и выберите Требования (Requirements). Откроется панель Требования (Requirements). Расшириться thrust_reverser_safety_requirements.
Требования безопасности связаны с блоками утверждения в подсистеме свойств безопасности. Блоки утверждения считаются целями доказательства. Статус проверки для каждого требования отражает результаты анализа свойств соответствующего блока Assertion.
3. Просмотрите статус проверки для требований. Щелкните правой кнопкой мыши одно из требований в браузере и выберите «Статус проверки». Столбец «Проверено» указывает, что требования не выполнены.
4. Проанализируйте свойства модели. На вкладке «Приложения» выберите «Проверка проекта». На вкладке Design Verifier щелкните Доказать свойства.
По завершении анализа свойств нажмите кнопку «Обновить», чтобы обновить статус в столбце «Проверено». Результаты показывают, что три из четырех целей фальсифицированы - анализ обнаружил состояние сигнала, которое фальсифицирует свойства и, следовательно, нарушает требования.
В окне Сводка результатов проверки конструкции (Design Verifier Results Summary) щелкните HTML, чтобы открыть подробный отчет об анализе. В главе 4 каждая фальсифицированная собственность содержит контрпример. Например, в контрпример, который фальсифицирует требование скорости полета:
При t = 0,1 разворачивается реверсивное устройство со скоростью ниже пороговой.
При t = 0,2 реверсивное устройство по-прежнему разворачивается со скоростью выше пороговой.
Временной ряд контрпримера указывает на состояние, которое может быть трудно встретить при моделировании, но, тем не менее, вызывает поведение модели, которое нарушает требование. Исследуйте поведение, анализируя зависимости сигналов в контрпример:
1. На вкладке «Проверка проекта» нажмите кнопку «Выделить в модели».
2. Выберите допустимый блок подтверждения скорости воздуха в подсистеме «Test Unit > Safety Properties > airspeed property».
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 диаграмма.
Дополнительное проектное требование предусматривает, что реверсивное устройство должно быть развернуто после паузы. Переработанная модель включает в себя:
Дополнительное aboutToBeDeployed состояние.
Расширенные условия перехода, возвращающиеся к undeployed.
Создайте связи между блоками проверки в переработанной модели и требованиями:
1. В модели на вкладке Приложения щелкните Диспетчер требований.
2. На вкладке Требования (Requirements) щелкните Редактор требований (Requirements Ed
3. Открытый thrust_reverser_safety_requirements в редакторе требований.
4. Для требования 1.1, Условие скорости воздуха, ссылка на действительный блок скорости воздуха в подсистеме свойств безопасности > Скорость воздуха. Перетащите R1.1 из браузера требований в допустимый блок скорости полета в модели.
5. Новая ссылка появится в редакторе требований на панели «Сведения» в разделе «Связи».
6. Удалите связь с блоком утверждения в исходной модели. Если исходная модель закрыта, эта связь выглядит неразрешенной. Рядом со ссылкой щелкните значок «Удалить ссылку».
7. Повторите действия для трех других требований и блоков проверки в переработанной модели.
Выполните анализ свойств для пересмотренной модели. Просмотрите результаты на панели Требования.
Результаты показывают, что свойства являются допустимыми.