Требования к программному обеспечению бортовой аппаратуры и систем КТ-178B (1015672), страница 19
Текст из файла (страница 19)
В результате такого анализа можно:• Получить доказательства, подтверждающие, что система является полной иправильной относительно предъявляемых требований.• Установить, что код, требования к ПО или архитектура ПО удовлетворяюттребованиям к ПО следующего более высокого уровня.© НИИАО 2002.Формат А474КТ-178В________________________________________________________________________________Цель применения формальных методов – предотвратить и исключить ошибки втребованиях, а также проекте и коде при выполнении процессов разработки ПО.Таким образом, формальные методы дополняют испытания.В испытаниях доказывается соответствие требованиям и выявляются ошибки, аформальные методы могут быть использованы для повышения уверенности в том, чтоненормальная работа невозможна или маловероятна для входных данных, выходящих запределы диапазона.Формальные методы могут использоваться в процессах разработки ПО с учетом:• Уровней проработки проекта.Использование формальных методов начинается с формулирования требованийвысокого уровня к ПО на формальном языке спецификаций и верификации посредствомформальных доказательств, что они удовлетворяют требованиям к системе, в особенности,ограничения, определяющие область нормальной работы.Затем показывается, что требования следующего более низкого уровня удовлетворяюттребованиям высокого уровня.Продолжение этого процесса до «Исходного кода» позволяет получить доказательства,что ПО удовлетворяет требованиям к системе.
Применение формальных методов можетначинаться и заканчиваться на последовательных уровнях проработки проекта представлениемдоказательств, что уровни требований установлены правильны.• Покрытия требований и архитектуры ПО.Формальные методы могут применяться к требованиям к ПО, которые:- Относятся к безопасности.- Могут быть определены с помощью дискретной математики.- Связаны со сложными режимами работы - такими, как согласование заданий,распределённая обработка, управление резервированием и синхронизация.Эти критерии могут применяться для того, чтобы определить набор требований на уровнепроработки проекта, для которого применяются формальные методы.• Степени строгости.Формальные методы имеют следующие последовательно возрастающие степенистрогости:- Формальные спецификации без доказательств.- Формальные спецификации с доказательствами вручную.- Формальные спецификации с автоматически проверяемыми доказательствами.Использование только формальных спецификаций гарантирует непротиворечивостьтребований.Получение доказательств с помощью «ручных» методов – хорошо понятный процесс,который можно применять при небольшой степени детализации.Автоматическая проверка правильности требований или автоматическоеформулирование доказательств может способствовать «ручным» методам получениядоказательств и может обеспечить более высокую степень надёжности, в особенности для болеесложных доказательств.12.3.2.
Испытания по методу полного перебораСуществуют ситуации, когда компоненты ПО бортовой системы и оборудования просты иизолированы друг от друга настолько, что набор входных и выходных данных может бытьограничен.В таких случаях можно продемонстрировать, что испытания по методу полного переборавходных сигналов могут заменить мероприятия, проводимые для доказательства соответствия ПОпредъявляемым требованиям.При использовании этого альтернативного метода Заявителю следует:а.
Дать полное определение совокупности достоверных входных и выходных данных ПО.b. Провести анализ, подтверждающий изолированность входных данных, поступающих вПО.© НИИАО 2002.Формат А475КТ-178В________________________________________________________________________________с. Дать обоснование полноты перебора входных данных и процедур испытаний.d. Указать тестовые примеры, процедуры и результаты испытаний.12.3.3.
Указания по верификации многоверсионного разнородного ПОСледующие указания относятся к процессу верификации ПО, когда он применяется кмноговерсионному разнородному ПО.Если в процесс верификации ПО внесены изменения, связанные с использованиеммноговерсионного разнородного программного обеспечения, то следует доказать, что цели такогопроцесса верификации и эквивалентный уровень обнаружения ошибок достигаются для каждойверсии ПО.Множество разнородных версий ПО создается использованием комбинации следующихметодов:• «Исходный код» составляется на двух или более различных языках кодирования.• Объектный код генерируется двумя или более различными компиляторами.• Каждая версия «Исполняемого объектного кода» выполняется на отдельномотличающемся процессоре или на одном процессоре, но с помощью средств, обеспечивающихобособление версий.• Требования к ПО, проект программного обеспечения и/или «Исходный код»разрабатываются двумя или более группами разработчиков, взаимодействие которыхкоординируется.• Требования к ПО, проект ПО и/или «Исходный код» разрабатываются сиспользованием двух или более сред разработки и/или каждая версия верифицируется сиспользованием отдельной среды испытаний.• «Исполняемый объектный код» редактируется и загружается двумя или болееразличными редакторами связей и загрузчиками.• Требования к ПО, проект ПО и/или «Исходный код» разрабатываются в соответствии сдвумя или более различными «Стандартами на разработку требований к ПО», «Стандартами напроектирование ПО» и/или «Стандартами на кодирование» соответственно.Если используется многоверсионное ПО, то методы верификации программногообеспечения могут отличаться от тех, которые используются для верификации одноверсионногоПО.Такие методы применяются для выполнения мероприятий процесса разработки ПО,которые разделяются на несколько ветвей, таких, как мероприятия, проводимые отдельнымигруппами.Процесс верификации ПО зависит от архитектуры объединённых аппаратных средств иПО, поскольку архитектура влияет на отличия в нескольких реализуемых версиях.Дополнительные цели процесса верификации, которые при этом необходимо достичь,следующие:а.
Продемонстрировать удовлетворение требований к внутренней совместимости версий,включая совместимость при нормальной и ненормальной работе, а также при переходныхпроцессах.b. Продемонстрировать, что достигается эквивалентное обнаружение ошибок.С сертифицирующим органом могут быть согласованы и другие изменения в процессеверификации ПО, если эти изменения обоснованы доказательством того, что эквивалентноепокрытие верификации ПО достигается.12.3.3.1.
Независимость многоверсионного разнородного ПОЕсли версии многоверсионного разнородного ПО разрабатываются независимо сиспользованием некоторого метода организации, то появляется потенциальная возможностьвыявить определённые классы ошибок, таких, что верификация каждой версии программногообеспечения будет эквивалентна независимой верификации процессов разработки ПО.© НИИАО 2002.Формат А476КТ-178В________________________________________________________________________________Для применения такого потенциального подхода инструкции относительно независимостиследующие:а.
Заявитель должен продемонстрировать, что требования к ПО, проект ПО и «Исходнойкод» для каждой версии ПО разработаны различными группами специалистов с ограничениями навзаимодействие групп.b. Анализ покрытия испытаний должен быть так же выполнен, как для одной версии.12.3.3.2. Верификация ПО, реализуемого на нескольких процессорахЕсли каждая версия разнородного ПО реализуется на процессоре разного типа, товерификация некоторых аспектов совместимости кода с процессором (п. 6.4.3.а) может бытьзаменена верификацией, гарантирующей, что процессоры разных типов формируют правильныевыходные данные.Эта верификация состоит из испытаний интеграции, в которых выходные данные разныхпроцессоров перекрёстно сравниваются между собой в тестовых примерах на основе требований.Заявителю следует показать, что:а.
Достигается эквивалентное обнаружение ошибок.b. Каждый процессор спроектирован независимым разработчиком.с. Выходные данные разных версий ПО эквивалентны.12.3.3.3. Верификация многоверсионного «Исходного кода»Для многоверсионного разнородного ПО бортовой системы или оборудования винструктивный материал, касающийся анализа структурного покрытия (п. 6.4.4.2) могут бытьвнесены изменения.Анализ структурного покрытия может выполняться на уровне «Исходного кода» даже втех случаях, когда нет непосредственной трассируемоети объектного кода на операторы«Исходного кода», при условии, что Заявитель покажет, что:а.
Каждая версия ПО написана с использованием отличающегося языкапрограммирования.b. Каждый используемый компилятор создан независимым разработчиком.12.3.3.4. Квалификация инструмента для многоверсионного разнородного ПОЕсли применяется многоверсионное разнородное ПО, то в процесс квалификацииинструмента могут быть внесены изменения при наличии доказательств, что для разработкиразных версий ПО используются разные инструменты.Это зависит от демонстрации эквивалентных мероприятий процесса верификации ПО врассматриваемой разработке различных версий ПО с использованием разнородных инструментовразработки.Заявителю следует показать, что:а. Каждый инструмент получен от разного разработчика.b.
Каждый инструмент выполнен по разному проекту.12.3.3.5. Применение нескольких имитаторов при верификацииЕсли для верификации многоверсионного разнородного ПО используются различныеразнородные имитаторы, то в квалификацию инструмента и имитатора могут быть внесеныизменения.Это зависит от демонстрации эквивалентности мероприятий верификации ПО примоделировании нескольких версий ПО с использованием различных имитаторов.© НИИАО 2002.Формат А477КТ-178В________________________________________________________________________________За исключением случаев, когда удаётся доказать, что это не является необходимым длянескольких разнородных имитаторов, следует представить доказательства, подтверждающие, что:а. Каждый имитатор разработан отдельной группой.b.
Каждый имитатор разработан с использованием различных требований, отличаетсяпроектами, отличается языком программирования.с. Каждый имитатор реализуется на различном процессоре.Примечание: Если в многопроцессорной системе, имеющей несколько разнородныхверсий ПО, используются одинаковые процессоры, то могут быть трудности в демонстрацииразнородности имитаторов из-за информации, получаемой из одного источника, каковым являетсяразработчик процессора.12.3.4.
Модели надёжности ПОВ процессе подготовки данного документа изучались методы оценки вероятностипрограммных ошибок, оставшихся не выявленными после верификации.Это делалось с целью разработки количественных требований к вероятности такихошибок в бортовых цифровых системах и оборудовании.Однако, согласно полученному заключению, существующие в настоящее время методыне обеспечивают результатов, достоверность которых соответствовала бы уровню, требуемомудля этой цели.Соответственно, в данном документе нет инструктивного материала относительноинтенсивности ошибок в ПО.Если для получения сертификационного зачета Заявитель предлагает использоватьмодели надёжности ПО, то обоснование их применимости должно быть включено в «Плансертификации ПО» и согласовано с сертифицирующим органом.12.3.5.
Заархивированный период эксплуатацииЕсли на основе заархивированного периода эксплуатации можно продемонстрировать,что обеспечивается эквивалентный уровень безопасности ПО, то это может быть учтено приполучении сертификационного зачёта.Приемлемость этого метода зависит от:• Управления конфигурацией ПО.• Эффективности мероприятий сообщений о проблемах.• Стабильности и «зрелости» ПО.• Репрезентативности условий заархивированного периода в эксплуатации.• Действительных интенсивностей ошибок заархивированного периода эксплуатации.• Влияния изменений.Указания относительно использования заархивированного периода эксплуатацииследующие:а.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
