При систематической проверке модели проекта на соответствие требованиям процесс разработки включает в себя генерацию тестов для каждого требования. Эти тесты подтверждают модель проекта, которая используется для генерации производственного кода, и помогают получить доверие, что модель проекта удовлетворяет требованиям. Модель спецификации является исполняемой сущностью, которая позволяет вам выполнять основанное на требованиях проверку, используя Simulink® Проектируйте Verifier™ возможности.
Если у вас есть набор требований, которые записаны в тексте на естественном языке, можно преобразовать их в формальные (исполняемые) спецификации с помощью Simulink. Затем они становятся моделью спецификации. В отличие от модели проекта, модель спецификации задает только То, что должно быть сделано, а не то, Как это должно быть сделано. Он фиксирует требования на более высоком уровне и скрывает детали на более низком уровне.
Преимуществами использования модели спецификации являются:
Он систематически проверяет набор требований.
Это автоматизирует проверку на основе требований.
Это помогает идентифицировать недостающие требования, ошибки проектирования или несоответствия в ваших требованиях и модели проекта в начале фазы разработки.
Для основанных на требованиях проверки, тесты, сгенерированные из модели спецификации, используются для проверки модели проекта на соответствие требованиям. Выполните следующие шаги для основанного на требованиях проверки с использованием модели спецификации:
Требования к автору в редакторе требований. Напишите свои требования в тексте на естественном языке, который описывает поведение системы, находящейся под проект.
Создайте модель спецификации. Проектируйте модель спецификации как исполняемое представление требований. Эта деятельность может выявить проблемы, которые приводят к уточнению требований.
Ссылки связи. Соедините отдельные требования или подзапросы с частями модели спецификации.
Сгенерируйте тесты для модели спецификации. Сгенерируйте по крайней мере один тест на каждое требование, которое демонстрирует его соответствие этому требованию.
Создайте подсистему тестового преобразования. Спецификация и модели проекта могут не использовать один и тот же интерфейс ввода-вывода. Преобразуйте тесты, которые были сгенерированы на шаге 4, с помощью системы тестового преобразования.
Разрабатывайте модель проекта. Разрабатывайте модель проекта самостоятельно с помощью документа требований. Привязать требования к модели проекта.
Проверьте проект и проанализируйте покрытие. Запустите тесты, сгенерированные на шаге 5, на модель проекта, которая была разработана на шаге 6, и проверьте, согласуются ли результаты с моделью спецификации и требованиями. Сгенерируйте отчет о модели проекта покрытии, чтобы идентифицировать недостающее покрытие и уточнить требования, при необходимости.
Рабочий процесс модели спецификации
Рассмотрим модели контроллеров автопилота, описанную в разделе «Использование модели спецификации для основанных на требованиях Проверок». Для этой демонстрации требования состоят из логических и временных условий разомкнутого контура.
Выполните следующие шаги, чтобы создать модель спецификации для требований:
Используйте высокоуровневое представление для значений сигналов
Идентифицируйте предусловия, эффекты и ожидаемый выход для каждого требования
Перечислите входные и выходные сигналы для модели спецификации, которые связаны с требованиями. Можно игнорировать сигналы, которые не связаны с существующими требованиями.
Это входные сигналы для контроллера автопилота, которые основаны на требованиях:
Autopilot Engage Switch: включите/отключите контроллер автопилота
Heading Engage Switch: При включении включает HDG_HOLD_MODE. В противном случае ROLL_HOLD_MODE активно
Roll Reference Target Turn Knob: циферблат, который подает желаемое значение угла крена на контроллер автопилота
Heading Reference Turn Knob: Задает значение уставки для режима заголовка
Угол крена самолета: Текущий мгновенный угол крена самолета
Это выходные сигналы:
Команда Элерона: Выход на привод элерона
Крен Ref Команды: Выход в окне отображения, указывающее заданное значение для привода элерона
Некоторые сигналы представлены на более высоком уровне в спецификациях. Рекомендуется представлять сигналы, используя высокоуровневое представление, подобное областям значений в модели спецификации.
Рассмотрим входной сигнал Угол крена самолета, который представляет текущий угол крена самолета и принимает любое значение в интервале от -180 до + 180 степени.
Требования описывают поведение контроллера автопилота в терминах зон. Эти зоны моделируются с помощью перечисления Range.
Эти пять зон показаны на следующем рисунке.
Требования определяют высокоуровневые режимы AP Controller и их активные условия следующим образом:
| Режим автопилота | Переключатель включения автопилота | Переключатель зацепления с заголовком |
|---|---|---|
OFF | ПРОЧЬ | Не волнуйтесь |
ROLL_HOLD_MODE | НА | ПРОЧЬ |
HDG_HOLD_MODE | НА | НА |
Примите во внимание следующее требование:
"Всякий раз, когда ручка поворота кабины Roll Reference Target Turn Knob (Roll_Ref_TK) командует в нормальной области значений (между [-30, -3] или [+ 3, + 30] степенями), Ссылка крена (Roll_Ref_Cmd) устанавливается в Roll_Ref_TK."
Определите предусловие и эффекты. Вышеуказанное требование состоит из двух пунктов:
Предусловие: Roll_Ref_TK находится или в отрицательной нормальной области значений, [-30, -3], или в положительной нормальной области значений, [+ 3, + 30 ].
Это предусловие является простым логическим выражением ИЛИ, поэтому таблицы истинности используются, чтобы выразить логические предусловия.
Эффект: Задать Roll_Ref_Cmd на Roll_Ref_TKПредложение эффекта задает выход значений сигналов в ожидаемом диапазоне.
Предложение предусловия требования определяет, когда оно становится активным, в то время как предложение эффекта определяет, что требование будет сделано после того, как оно станет активным.
Вышеуказанное требование не влияет на Команду Элерона Ail_Cmd выход, поэтому он рассматривается как Range.All который обозначает набор всех возможных значений.
Составьте таблицу истинности для требований
Закодируйте предложение предусловия требования в разделе «Таблица условий» таблицы истинности и предложение эффекта в разделе «Таблица действий».
Для индивидуального отслеживания каждого требования установите REQ_ID локальной переменной соответствующий идентификатор требования 2.1.
Добавьте цель Simulink Design Verifier в Таблицу действий с помощью оператора sldv.test (REQ_ID==2.1). Simulink Design Verifier находит тест, когда REQ_ID 2.1 удовлетворена.
Итоговая модель спецификации, полученная при помощи вышеописанного рабочего процесса, выглядит следующим образом:
Используйте модель спецификации для основанного на требованиях проверки
