${message}

Верификация кода критических систем c LDRA

  Трассируемость требования-код-тесты  Статистический анализ  Модульное тестирование  Интеграционное тестирование  Верификация исполняемого объектного кода  Квалификация инструментов 

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

Компании, которые уже используют LDRA:









В зависимости от отрасли применяются следующие стандарты для создания безопасного программного обеспечения:

  • Авиастроение: DO-178/КТ-178, DO-278, DO-254/КТ-254, ARP4754A/Р4754А, ARP4761
  • Автомобилестроение: ISO 26262
  • Медицинская техника: IEC 62304
  • Железные дороги: EN 50128
  • Промышленная автоматизация: ГОСТ Р МЭК 61508, IEC 61508
  • Атомная энергетика: IEC 60880, IEC 61513
  • Встраиваемые системы: ГОСТ Р 51904, ГОСТ РВ 0019-001-2006

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

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

Набор инструментов LDRA обеспечивает непротиворечивый и целостный процесс верификации ПО - от управления трассируемостью до квалификации инструмента для удовлетворения самим строгим требованиям отраслевых стандартов


"LDRA крайне полезен, когда у разработчика строго определена спецификация требований, и требования не меняются еженедельно. В таком случае LDRA позволяет покрыть код и требования тестами, проверить полноту покрытия и в конечном счете подтвердить соответствие ПО определённому уровню критичности. ГосНИИАС использует LDRA для выполнения статистического анализа, сбора покрытия в режиме system test и оптимизации ПО."


Запрос консультации

Трассируемость: требования <-> код <-> тесты

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

При помощи набора инструментов LDRA устанавливается трассируемость между требованиями, кодом и тестами.

Программное обеспечение

Статический анализ

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

Статический анализатор, входящий в набор инструментов LDRA, анализирует исходный код на соответствие популярным или пользовательским стандартам кодирования и рассчитывает метрики исходного кода.

Программное обеспечение

Модульное тестирование

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

  • Тестовые вектора недостаточны (неполны)
  • Требования к ПО недостаточны (неполны)
  • Выявлен неисполняемый код

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

Набор инструментов LDRA включает возможности проведения модульного тестирования, основанного на требованиях, со сбором покрытия и автоматического создания тестов на робастность.

Интеграционное тестирование

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

Набор инструментов LDRA позволяет проводить тестирование интеграции ПО со сбором покрытия его тестами на целевой платформе и анализировать нарушения интеграции.

Верификация исполняемого объектного кода

После работы компилятора, компоновщика и ассемблера итоговый исполняемый объектный код не соответствует исходному коду, созданному на языке высокого уровня. Иными словами на уровне объектного кода появляется код, не трассирующийся на требования. Для самых критичных к безопасности систем стандарты предписывают выполнять анализ структурного покрытия не по исходному, а по исполняемому объектному коду (например, см. цель A-7.9 КТ-178С).

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

Квалификация инструментов

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

Программное обеспечение

Задать вопрос

*
Настоящим в соответствии с Федеральным законом № 152-ФЗ «О персональных данных» от 27.07.2006, отправляя данную форму, вы подтверждаете свое согласие на обработку персональных данных . Мы, ООО ЦИТМ "Экспонента" и аффилированные к нему лица, гарантируем конфиденциальность получаемой нами информации. Обработка персональных данных осуществляется в целях эффективного исполнения заказов, договоров и пр. в соответствии с «Политикой конфиденциальности персональных данных». * - обязательные поля