Сертификация и разработка систем повышенной надежности

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

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

Simulink Requirements предоставляет интерфейс для управления требованиями, который позволяет связаться с любой системой управления требованиями. По умолчанию поддерживаются IBM DOORS, Word, Excel и многие другие. Кроме того, доступен Requirements Editor, позволяющий разрабатывать требования непосредственно в Simulink.

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

Ключевые особенности:

• Simulink и Stateflow для разработки алгоритмов и управляющей логики в соответствии с требованиями высокого уровня
• Simulink Requirements для связи модели с требованиями и обеспечения двусторонней трассируемости между требованиями низкого уровня и требованиями высокого уровня
• Simulink Report Generator для автоматизированного создания описания проекта ПО, содержащего требования низкого уровня и архитектуру ПО

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

Вы устанавливаете стандарты моделирования и проверяете модели на соответствие этим стандартам при помощи инструмента Model Advisor. Simulink Check предоставляет набор проверок по DO-178, MAAB и другим стандартам моделирования, которые позволяют выявить проблемы моделирования, уделить внимание генерации критичного к безопасности кода, максимизировать использование встроенных диагностик Simulink и Stateflow во время симуляции и сделать их наиболее строгими. Отчет Simulink Check является одним из артефактов для сертификации и позволяет вам доказать, что требования низкого уровня и архитектура ПО правильны и непротиворечивы, и соответствуют установленным стандартам.

Ключевые особенности:

• Использование встроенных проверок Simulink Check для проверки моделей на соответствие стандартам моделирования
• Создание собственных проверок и правил моделирования
• Готовые стандарты моделирования с привязкой к целям DO-178

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

Вы проверяете ваши модели относительно требований высокого уровня. Вы создаете тестовые вектора на основании требований и описываете входы и ожидаемые выходы. Simulink Test позволяет автоматизировать тестирование, а Simulink Report Generator помогает автоматизировать создание отчетов.

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

Simulink Design Verifier также позволяет при помощи формальных, то есть математических, методов доказать определенные свойства системы. Например, что заданный сигнал всегда будет в указанном диапазоне. Simulink Design Verifier сгенерирует автоматизированные отчеты, а если то или иное свойство не выполняется, сгенерирует контр-пример. При помощи Simulink Design Verifier вы можете автоматически сгенерировать тестовые вектора для 100% покрытия модели тестами по MC/DC.

Ключевые особенности:

• Использование Simulink Test для систематического тестирования моделей
• Использование Simulink Coverage для анализа покрытия моделей тестами и оценки полноты тестирования
• Использование Simulink Design Verifier для автоматической генерации тестов и формальной верификации модели

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

Из модели генерируется исходный код при помощи Embedded Coder. Embedded Coder генерирует читаемый, компактный и быстрый C и C++ код для использования во встраиваемых процессорах, отладочных платах и микропроцессорах, используемых для серийного производства.

Embedded Coder активирует дополнительные настройки конфигурации для MATLAB Coder и Simulink Coder, а также включает продвинутые оптимизации для тонкой настройки функций, файлов и данных в сгенерированном коде. Эти оптимизации улучшают эффективность кода и облегчают интеграцию с существующим кодом, типами данных и калибровочными параметрами, используемыми в производстве. Вы можете подключить стороннюю среду разработки к процессу сборки, чтобы получить исполняемый файл "под ключ" для развертывания на вашей встраиваемой системе.

Для генерации VHDL или Verilog кода используется HDL Coder. HDL Coder генерирует синтезируемый код для ПЛИС с побитовым и цикловым соответствием исходной модели Simulink.

Верификация HDL кода относительно модели осуществляется при помощи HDL Verifier. HDL Verifier поддерживает верификацию с HDL симуляторами (ко-симуляция) и верификацию на реальном железе в режиме ПЛИС-в-контуре (FPGA-in-the-Loop).

Ключевые особенности:

• Читаемый, портируемый (независимый от Simulink), компактный и быстрый С/С++ код из моделей Simulink
• Синтезируемый, стандартный VHDL или Verilog код для ПЛИС
• Интеграция с распространенными отладочными платами и средами разработки
• Возможность тонкой настройки генератора кода и интеграции с вашим целевым вычислителем
• Поддержка систем на кристалле: Intel (Altera) SoC и Xilinx Zynq

Ознакомьтесь со следующими материалами для получения дополнительной информации.

Embedded Coder обеспечивает трассируемость исходного кода к требованиям низкого уровня, т.е. модели.

Вы можете сгенерировать матрицу трассируемости при помощи Simulink Code Inspector, которая является одним из артефактов для сертификации и устанавливает соответствие между каждым элементом модели и операцией в коде и наоборот.

Simulink Code Inspector предоставляет независимую верификацию того, что код, сгенерированный Embedded Coder, отслеживается и соответствует низкоуровневым требованиям. Это демонстрирует, что модель и исходный код соответствует структурно и функционально, а также уменьшает или полностью устраняет необходимость ручного рассмотрения и анализа кода.

Ключевые особенности:

• Исключение или упрощение ручного анализа кода, который был получен из модели
• Двусторонняя независимая инспекция на структурное и функциональное соответствие модели и кода
• Автоматизация мероприятий по верификации кода из DO-178

Ознакомьтесь с материалами ниже, чтобы получить больше информации.

Вы проверяете исходный код на соответствие стандартам кодирования. MISRA-C – это один из распространенных стандартов, используемых как основа при сертификации по DO-178 и другим стандартам разработки.

Polyspace Bug Finder – это инструмент, позволяющий проверять исходный код на соответствие стандарту MISRA-C и другим стандартам, а также добавлять собственные правила. Проверки Polyspace Bug Finder по MISRA-C квалифицируются по DO-178 и позволяют получить вам соответствующие артефакты для сертификации в виде отчетов.

Ключевые особенности:

• Проверки кода на соответствие стандартам кодирования
• Измерение метрик (характеристик) исходного кода, влияющих на читаемость, тестируемость и безопасность
• Создание собственных правил кодирования

Ознакомьтесь с материалами ниже, чтобы получить больше информации.

Формальные методы верификации кода в Polyspace Code Prover позволяют доказывать отсутствие ошибок времени исполнения и анализировать мертвые ветки кода. Отчеты по формальной верификации Polyspace являются артефактами для сертификации, позволяющими вам получить сертификационные зачеты за использование формальных методов, как описано в DO-333.

Ключевые особенности:

• Применение формальных методов для доказательства свойств кода, в том числе в контексте стандарта DO-333
• Доказательство качества работы вашей системы в широком диапазоне рабочих условий
• Глубокая верификация исходного кода при помощи метода "абстрактной интерпретации"

Ознакомьтесь с материалами ниже, чтобы получить больше информации.

Вы получаете объектный код при помощи компилятора или среды разработки, предоставленной разработчиком процессора. Полученный объектный код верифицируется относительно модели, или низкоуровневых требований, при помощи методики Процессор-в-Контуре (или Processor-in-the-Loop). При этом вы повторно используете те же самые тестовые вектора, что и во время симуляции модели. Для низкоуровневого тестирования или для тестирования на робастность могут повторно использоваться тесты, автоматически сгенерированные при помощи Simulink Design Verifier на уровне модели. Дополнительно осуществляется анализ покрытия кода тестами при помощи Simulink Coverage и анализ производительности исполняемого кода при помощи профилирования времени выполнения.

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

Ключевые особенности:

• Использование методики Процессор-в-Контуре для верификации функциональной эквивалентности модели и сгенерированного и скомпилированного кода
• Использование методики Процессор-в-Контуре для анализа покрытия кода тестами и профилирования времени выполнения
• Повторное использование высокоуровневых (функциональных) тестов и низкоуровневых тестов, разработанных на уровне модели

Ознакомьтесь с материалами ниже, чтобы получить больше информации.

Для квалификации инструментов, поддерживающих верификацию по DO-178, предлагается инструмент DO Qualification Kit. Этот набор включает необходимые документы, тестовые модели и код, процедуры тестирования и ожидаемые результаты.

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

IEC Certification Kit содержит информацию о сертификации и квалификации инструментов разработки и верификации для процессов разработки по стандартам IEC 61508 и ISO 26262.

Ключевые особенности:

• Квалифицируемые инструменты верификации по DO-178/КТ-178/DO-331/КТ-331
• Сертифицированные и квалифицированные инструменты разработки и верификации по IEC 61508/ISO 26262
• Упрощение мероприятий квалификации и использование квалифицированных инструментов в процессе разработки и верификации

Ознакомьтесь с материалами ниже, чтобы получить больше информации.