Что такое модель спецификации?

При систематической проверке модели проекта на соответствие требованиям процесс разработки включает в себя генерацию тестов для каждого требования. Эти тесты подтверждают модель проекта, которая используется для генерации производственного кода, и помогают получить доверие, что модель проекта удовлетворяет требованиям. Модель спецификации является исполняемой сущностью, которая позволяет вам выполнять основанное на требованиях проверку, используя Simulink® Проектируйте Verifier™ возможности.

Если у вас есть набор требований, которые записаны в тексте на естественном языке, можно преобразовать их в формальные (исполняемые) спецификации с помощью Simulink. Затем они становятся моделью спецификации. В отличие от модели проекта, модель спецификации задает только То, что должно быть сделано, а не то, Как это должно быть сделано. Он фиксирует требования на более высоком уровне и скрывает детали на более низком уровне.

Преимуществами использования модели спецификации являются:

  • Он систематически проверяет набор требований.

  • Это автоматизирует проверку на основе требований.

  • Это помогает идентифицировать недостающие требования, ошибки проектирования или несоответствия в ваших требованиях и модели проекта в начале фазы разработки.

Использование моделей спецификации для основанного на требованиях проверки

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

  1. Требования к автору в редакторе требований. Напишите свои требования в тексте на естественном языке, который описывает поведение системы, находящейся под проект.

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

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

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

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

  6. Разрабатывайте модель проекта. Разрабатывайте модель проекта самостоятельно с помощью документа требований. Привязать требования к модели проекта.

  7. Проверьте проект и проанализируйте покрытие. Запустите тесты, сгенерированные на шаге 5, на модель проекта, которая была разработана на шаге 6, и проверьте, согласуются ли результаты с моделью спецификации и требованиями. Сгенерируйте отчет о модели проекта покрытии, чтобы идентифицировать недостающее покрытие и уточнить требования, при необходимости.

Рабочий процесс модели спецификации

Создание модели спецификации

Рассмотрим модели контроллеров автопилота, описанную в разделе «Использование модели спецификации для основанных на требованиях Проверок». Для этой демонстрации требования состоят из логических и временных условий разомкнутого контура.

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

Идентифицируйте интерфейс модели спецификации

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

Это входные сигналы для контроллера автопилота, которые основаны на требованиях:

  1. Autopilot Engage Switch: включите/отключите контроллер автопилота

  2. Heading Engage Switch: При включении включает HDG_HOLD_MODE. В противном случае ROLL_HOLD_MODE активно

  3. Roll Reference Target Turn Knob: циферблат, который подает желаемое значение угла крена на контроллер автопилота

  4. Heading Reference Turn Knob: Задает значение уставки для режима заголовка

  5. Угол крена самолета: Текущий мгновенный угол крена самолета

Это выходные сигналы:

  1. Команда Элерона: Выход на привод элерона

  2. Крен 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."

Определите предусловие и эффекты.  Вышеуказанное требование состоит из двух пунктов:

  1. Предусловие: Roll_Ref_TK находится или в отрицательной нормальной области значений, [-30, -3], или в положительной нормальной области значений, [+ 3, + 30 ].

    Это предусловие является простым логическим выражением ИЛИ, поэтому таблицы истинности используются, чтобы выразить логические предусловия.

  2. Эффект: Задать 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 удовлетворена.

Окончательная модель спецификации

Итоговая модель спецификации, полученная при помощи вышеописанного рабочего процесса, выглядит следующим образом:

См. также

Документация Simulink Design Verifier

Поддержка

Для просмотра документации необходимо авторизоваться на сайте