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

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

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

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

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

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

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

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

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

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

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

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

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

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