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

Авторы - Н.В. Богославский, В.М. Понятский, В.Г. Федорищева

Рассмотрена технология проверки разрабатываемой системы управления на ранней стадии проектирования c использованием инструментов MathWorks. Технология поддерживает реализацию подхода «от модели к программе» и включает процедуры создания связи модели с документом требований; проверку модели на соответствие стандартам моделирования; функциональное тестирование модели; анализ на покрытие модели тестами; проверку на ошибки проектирования; доказательство свойств модели и автоматическую генерацию тестов для 100%-ого покрытия модели.

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

Продукты MathWorks обеспечивают единую среду для разработки встраиваемого ПО, начиная от формирования требований и заканчивая созданием объектного кода и файлов прошивки микроконтроллера. Причем на всех этапах жизненного цикла проводится тестирование и верификация проектируемого ПО: требования (спецификация), модель (выполняемая спецификация), код, объектный код (см. рис.1). 

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

В продуктах MathWorks реализована поддержка двух стандартных подходов для верификации встраиваемого ПО: верификация от модели к программе и обнаружение ошибок при выполнении в исходном коде.

Рис. 1. Рабочий процесс разработки ПО с помощью инструментов MathWorks 

 

При подходе «от модели к программе» полностью верифицированная модель встраиваемой программы используется в качестве эталона для сравнения ее поведения с работой написанного вручную или автоматически сгенерированного из модели программного обеспечения. При использовании второго подхода при помощи продуктов MathWorks к написанному вручную или автоматически сгенерированному коду применяются формальные методы для проверки на наличие ошибок выполнения. Эти процедуры верификации особенно важны для встраиваемых систем с высокой степенью интеграции.

Рассмотрим первый подход к верификации на примере разработки встраиваемого ПО блока управления следящим приводом оптико-электронной системы.

Технология валидации и верификации модели с помощью инструментов MathWorks включает следующие процедуры:

• создание элементов модели и связей с требованиями (трассируемость);
• проверка на соответствие стандартам моделирования;
• функциональное тестирование модели;
• анализ на покрытие модели тестами;
• проверка на ошибки проектирования;
• доказательство свойств модели;
• автоматическая генерация тестов.

 

Создание связи элементов модели с требованиями

Simulink Verification and Validation – это пакет расширения Simulink для проведения полного комплекса тестирований и проверок систем с учетом технических требований. Требования к модели формируются на основе технического задания к разрабатываемой системе и не должны быть противоречивыми.  

Для управления требованиями в Simulink Verification and Validation есть инструмент Simulink Requirements. Этот инструмент способен импортировать требования из Word, Excel или устанавливать связь с системами электронного документооборота. Simulink Requirements позволяет связать требования с блоками модели Simulink, всей моделью или кодом, сгенерированным из модели.

После установки связи элементов модели с требованиями (см. рис.2), можно проанализировать требования на трассируемость, то есть отслеживаемость в модели.  

Рис. 2. Детализация связи блока модели с документом требований

 

Это возможно благодаря навигации из документа требований в модель и обратно (см. рис.3). 

Рис. 3. Навигация из документа требований в модель

 

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

 

Проверка на соответствие стандартам моделирования

Для повышения качества модели необходимо провести проверку на соответствие стандартам моделирования, например, на стандарт MathWorks Automotive Advisory Board (MAAB). MAAB является компанией, которая разрабатывает рекомендации по использованию и усовершенствованию средств управления, моделирования и генерации кода MathWorks, включая Simulink, Stateflow и Embedded Coder.

Инструкции стандарта MAAB важны для успеха проекта и работы в команде – и внутренней, и при сотрудничестве с партнерами или субподрядчиками. Соблюдение инструкций стандарта MAAB является ключевой предпосылкой к достижению:

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

Основные требования стандарта MAAB по единому стилю моделирования:

• правила именования (файлов, директорий, подсистем, блоков, портов, сигналов);
• архитектура модели (разделение Simulink и Stateflow, иерархия подсистем, декомпозиция);
• параметры конфигурации модели;
• типы данных и значения по умолчанию;
• правила создания безопасных конструкций Simulink, Stateflow, MATLAB Function.

Проверки на соответствие стандартам проводятся с помощью инструмента Model Advisor. На рис. 4 приведен фрагмент отчета о пройденных проверках на стандарт моделирования MAAB блока управления (ЦВС) модели оптико-электронной системы (ОЭС). Отчет содержит информацию о модели, дате создания и модификации, номер версии, результаты проверки, предупреждения и ошибки, а также рекомендации по их устранению.

Рис. 4. Фрагмент отчета о проверке на стандарт моделирования MAAB блока управления модели ОЭС

 

Функциональное тестирование модели

При функциональном тестировании модель выполняется с использованием тестовых сценариев, определяемых требованиями к модели. На рис. 5 показано использование функционального тестирования на этапах создания программного обеспечения от требований до кода. 

Тестовый сценарий состоит из входов модели, ожидаемых результатов выполнения модели и критериев оценки. 

Для проведения функционального тестирования используется инструмент Simulink Test. Simulink Test содержит инструменты для разработки тестов, управления тестами и выполнения тестов. Simulink Test включает  блок  Test  sequence, который позволяет создавать сложные тестовые последовательности и оценки выполнения тестов, а также менеджера по тесту Test Manager, который позволяет управлять выполнением тестов. В Test Manager есть несколько типов шаблонов тестового сценария.

Один из примеров выполнения функционального тестирования: тест Baseline. При выполнении этого теста выходные сигналы модели сравниваются с исходным набором сигналов (сравнение текущего результата моделирования с записанным результатом моделирования при номинальных значениях параметров модели). Сравнение текущего результата моделирования и baseline допускается в абсолютных или относительных допусках. Допуски задаются в разделе критериев тестового сценария.

Рис. 5. Функциональное тестирование на этапах создания ПО

 

Применительно к модели ОЭС тест baseline можно использовать для оценки влияния разброса параметров модели на выходные характеристики.

На рис.6-7 приведены результаты выполнения функционального теста baseline для оценки влияния разброса параметра NKU.

Рис. 6. Результаты выполнения функционального теста для канала ВН с номинальным значением константы NKU

 

Рис. 7. Результаты выполнения функционального теста для канала ВН с максимальным отклонением константы NKU от номинального значения

 

Анализ покрытия модели тестами

Инструмент Simulink Coverage выполняет анализ покрытия модели и кода тестами и измеряет полноту тестирования в моделях и сгенерированном коде. Он применяет метрики, такие как выполнение (execution), решение (decision), состояние (condition), модифицированное покрытие состояния/решения (MCDC) и реляционное пограничное покрытие для оценки эффективности имитационного тестирования в моделях, программном обеспечении в режимах «программа в контуре» (SIL-тестирование) и «процессор в контуре» (PIL-тестирование). Можно использовать данные о покрытии для поиска пробелов в тестировании, отсутствующих требований или непредвиденных функциональных возможностей.

Simulink Coverage осуществляет сбор покрытия тестами при запуске симуляции модели, а также в режимах SIL и PIL. 

Полнота покрытия тестами – важный параметр, показывающий, что компонент модели выполняет возложенные на него функции и полностью протестирован. Покрытые на 100% элементы модели подкрашиваются в модели зеленым цветом (см. рис.8).

Рис. 8. Анализ на покрытие тестами блока управления модели ОЭС: а) блоки модели верхнего уровня

 

Рис. 8. Анализ на покрытие тестами блока управления модели ОЭС: б) блоки диаграммы Stateflow

 

Если анализ покрытия элементов модели тестами показал, что покрытие модели неполное, используется режим Generate Test инструмента Simulink Design Verifier для генерации тестов для 100%-ого покрытия.

 

Проверка на ошибки проектирования

Simulink Design Verifier, используя методы формальной верификации, служит для нахождения ошибок проектирования, не требуя интенсивного тестирования или запуска симуляции модели. В отличие от традиционного тестирования, которое позволяет поместить систему в ограниченное число состояний, формальная верификация в идеальном случае охватывает все пространство состояний системы (модели). В действительности, формальная верификация охватывает значительную область пространства состояний системы.

Ошибки проектирования:

• мертвая логика;
• ошибки переполнения;
• деление на ноль;
• нарушение ограничений и требований к системе.

Simulink Design Verifier подсвечивает блоки, в которых доказано отсутствие ошибок и блоки, в которых выявлены ошибки выполнения. Для блоков с ошибками генерируется тестовый вектор, который позволяет воспроизвести ошибку во время симуляции. 

На рис.9 показаны результаты проверки блока управления модели ОЭС на наличие мертвой логики: в диаграмме Stateflow обнаружен переход, в отношении которого доказана неактивность во время моделирования.

Рис. 9. Переход с мертвой логикой в блоке управления модели ОЭС

 

 

Рис. 10. Модель обвязки с сформированными тестовыми векторами, подтверждающими наличие мертвой логики в блоке управления модели ОЭС

 

На рис. 10 показана модель обвязки, сгенерированная из модели ОЭС. Модель обвязки представляет собой источник входных сигналов и подсистему, в которой находится модель ОЭС. Тестовые вектора в блоке Signal Builder при моделировании подтверждают наличие неактивного перехода в диаграмме Stateflow.

 

Доказательство свойств системы

При работе в режиме доказательства свойств, Simulink Design Verifier может определять нарушения утверждений (assertions), например, что указанный сигнал не выйдет за границы диапазона. Simulink Design Verifier проверяет, существуют ли какие-то сценарии, которые могут вызвать нарушение утверждения во время симуляции за число шагов, указанное в настройках анализа. В дополнение к утверждениям, доступным в Simulink, Simulink Design Verifier предлагает дополнительные блоки для задания ограничений для анализа, что позволяет тщательно анализировать поведение системы и искать ошибки проектирования до запуска симуляции. Утверждение, которое может нарушаться, подсвечивается красным цветом, и генерируется тестовый вектор, который вызывает нарушение этого утверждения. 

Рис. 11. Окно результатов после проверки

 

Рис. 12. Окно с результатом: блок прошел проверку

 

На рис. 11-12 приведены результаты проверки утверждения, что значение сигнала внутри блока NKU не выйдет за пределы диапазона [-1;1].

 

Автоматическая генерация тестов для 100 %-ого покрытия

Генерация тестов для 100 %-ого покрытия модели дополняет функциональные тесты, основанные на требованиях (созданные вручную или собранные во время симуляции всей системы). При таком подходе Simulink Design Verifier берет информацию о существующем покрытии модели и генерирует дополнительные тестовые вектора, которые выполняют все цели покрытия, не удовлетворенные во время тестирования на основании требований.

После этапа валидации и верификации, модель, прошедшая проверки, для которой подтверждено соответствие предъявляемым требованиям, соответствие стандарту моделирования, доказано отсутствие ошибок проектирования, проведено тестирование и обеспечено 100%-ое покрытие тестами, может быть передана для разработки программного кода, который в дальнейшем будет прошит на микропроцессорной системе и использован на реальном объекте управления.

Генерация С-кода из моделей Simulink для процессоров встроенных систем осуществляется при помощи пакета Embedded Coder [1]. Генерируемый С-код может быть универсальным или специализированным, настроенным под определенный тип процессора. Процесс генерации С-кода включает следующие процедуры [1]:

• выбор параметров решателя;
• выбор целевого файла;
• выбор аппаратной реализации;
• выбор опций оптимизации кода;
• выбор дополнительных опций;
• генерация С-кода.

Поддержка аппаратной реализации обеспечена либо фирмой MathWorks, либо фирмами-производителями микроконтроллеров. В последнем случае для генерации кода под определенный микроконтроллер необходимо установить дополнительное ПО. Например, для создания C-кода для процессоров семейства STM32F4-Discovery выбрать в браузере файл ert.tlc Embedded Coder (рис.13), предварительно установив пакет поддержки STM32F4-Discovery.  

Рис. 13. Окно выбора целевого файла для генерации программного кода

 

Это можно сделать из меню Add-Ons -> Get Hardware Support Packages (рис. 14). 

Рис. 14. Окно меню Add-Ons

 

Либо скачать библиотеки Embedded Coder Support Package for STMicroelectronics Discovery Boards и Embedded Coder Support Package for ARM Cortex-M Processors с официального сайта MathWorks и автономно установить. Затем выбрать аппаратную реализацию и сгенерировать С-код для блока управления (ЦВС) модели ОЭС, выбрав в контекстном меню блока C/C++ Code -> Build Subsystem.

На рис.15 приведен фрагмент сгенерированного кода.

Рис. 15. Фрагмент С-кода, сгенерированного из блока управления модели ОЭС

 

Проведено сравнение результатов выполнения Simulink-модели ОЭС с Simulink-моделью, в которую вместо блока управления (ЦВС) добавлен С-код (рис.16).

Рис. 16. Результаты выполнения Simulink-модели ОЭС

 

Результаты выполнения модели с сгенерированным кодом не отличаются от результатов моделирования непрерывной Simulink-модели.

Для наглядности отображения результатов моделирования, возможности ввода данных и режимов работы в процессе моделирования, создается графический интерфейс пользователя. MATLAB предлагает два варианта реализации графического пользовательского интерфейса: 

• с помощью блоков библиотеки Simulink Dashboard; 
• с помощью инструмента App Designer. 

Создание интерфейса с помощью библиотеки Simulink Dashboard является более простым в реализации, а инструмент App Designer более гибкий и предоставляет больше возможностей. 

Таким образом, показана возможность применения  технологии верификации и валидации для подготовки модели к генерации С-кода. Технология апробирована на модели ОЭС. Из проверенной модели с использованием технологии генерации кода сгенерирован оптимизированный по времени выполнения и памяти С-код. 

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

 

Список литературы

1. Понятский В.М., Кушников Д.В., Федорищева В.Г. Методика генерации из моделей MATLAB текста программ на языке С для процессоров встроенных систем. 11-я международная конференция «Системы проектирования, технологической подготовки производства и управления этапами жизненного цикла промышленного продукта (CAD/CAM/PDM – 2011)». Москва, 18-20 октября 2011г. Сборник материалов / Под ред. Артамонова Е.И. − М: Институт проблем управления РАН, 2011. − С. 83−87.