В следующей таблице содержится сводная информация о проверке целей процесса кодирования и интеграции из DO-178C, DO-331, DO-332 и DO-333, включая цель, применимые справочные разделы и уровни программного обеспечения, применимые к цели. В таблице также описаны доступные инструменты конструирования на основе модели для достижения поставленных целей.
Таблица A-5: Проверка процесса кодирования и интеграции
| Цель | Справочные разделы | Справочные разделы по деятельности | Уровни программного обеспечения | Доступные продукты для конструирования на основе моделей | |
|---|---|---|---|---|---|
| 1 | Исходный код соответствует требованиям низкого уровня. | MB.6.3.4.a | MB.6.3.4 | A, B, C | Набор для проверки кода Simulink ® Inspector™, DO |
| 2 | Исходный код соответствует архитектуре программного обеспечения. | MB.6.3.4.b OO.6.3.4.b Из 6.3.4.b Из 6.3.a | MB.6.3.4 OO.6.3.4 ИЗ 6.3.4 | A, B, C | Simulink Code Inspector, Polyspace ® Code Prover™, Polyspace Code Prover Server™,Polyspace Code Prover Server, квалификационный комплект DO |
| 3 | Исходный код поддается проверке. | MB.6.3.4.c OO.6.3.4.c Из 6.3.4.c Из 6.3.e | MB.6.3.4 OO.6.3.4 ИЗ 6.3.4 | A, B | Инспектор кода Simulink, провайдер кода Polyspace, сервер проверочного кода Polyspace, квалификационный комплект DO |
| 4 | Исходный код соответствует стандартам. | MB.6.3.4.d OO.6.3.4.d Из 6.3.4.d Из 6.3.f | MB.6.3.4 OO.6.3.4 ИЗ 6.3.4 | A, B, C | Polyspace Bug Finder™, проверка кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
| 5 | Исходный код отслеживается в соответствии с требованиями низкого уровня. | MB.6.3.4.e | MB.6.3.4 | A, B, C | Инспектор кода Simulink, квалификационный комплект DO |
| 6 | Исходный код является точным и непротиворечивым. | MB.6.3.4.f OO.6.3.4.f Из 6.3.4.f Из 6.3.b Из 6.3.c | MB.6.3.4 OO.6.3.4 ИЗ 6.3.4 | A, B, C | Simulink Code Inspector, Polyspace Bug Finder, Polyspace Bug Finder Server, Polyspace Code Prover, Polyspace Code Prover Server, DO Qualification Kit |
| 7 | Вывод процесса интеграции программного обеспечения завершен и корректен. | 6.3.5.a | 6.3.5 | A, B, C | Неприменимо |
| 8 | Файл элемента данных параметра верен и завершен | 6.6.a | 6.6 | A, B, C, D | Неприменимо |
| 9 | Выполняется проверка файла элемента данных параметра. | 6.6.b | 6.6 | A, B, C | Неприменимо |
| FM 10 | Случаи и процедуры формального анализа верны. | Из 6.3.6.a Из 6.3.6.b | ИЗ 6.3.6 | A, B, C | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
| FM 11 | Результаты формального анализа верны, а расхождения объяснены. | Из 6.3.6.c | ИЗ 6.3.6 | A, B, C | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
| FM 12 | Формализация требований верна. | Из 6.3.i | Из 6.3.i | A, B, C | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
| FM 13 | Формальный метод правильно обоснован и уместен. | ИЗ 6.2.1 | Из 6.2.1.a Из 6.2.1.b Из 6.2.1.c | A, B, C, D | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
В следующих разделах более подробно описываются потенциальные последствия для каждой проверки целей процесса кодирования и интеграции при использовании модели проектирования, если применимо, по сравнению с традиционной разработкой.
Соответствие низкоуровневым требованиям можно проверить с помощью Simulink Code Inspector, который проверяет соответствие исходного кода требованиям модели.
Инспектор кода Simulink может быть квалифицирован с помощью квалификационного комплекта DO.
Соответствие архитектуре программного обеспечения можно проверить с помощью Simulink Code Inspector, который проверяет соответствие исходного кода архитектуре, определенной в модели.
Для рукописного кода, Polyspace Code Prover и Polyspace Code Prover Server доказывают приверженность архитектуре программного обеспечения, поскольку он анализирует использование глобальных переменных данных. На основе этого анализа инструмент автоматически создает глобальный словарь данных и определяет доступ к чтению и записи общих данных. Сервер проверки кода Polyspace и Сервер проверки кода Polyspace анализируют связи вызовов в исходном коде. На основе этого анализа инструмент автоматически вычисляет дерево вызовов приложения.
С помощью набора DO Qualification Kit можно квалифицировать Simulink Code Inspector, Polyspace Code Prover и Polyspace Code Prover Server.
Проверяемость кода можно проверить с помощью Simulink Code Inspector, который проверяет соответствие модели; Поскольку модель поддается проверке, код не нуждается в изменении для проверки.
Polyspace Bug Finder и Polyspace Bug Finder Server могут помочь в идентификации непроверяемых структур кода.
Polyspace Code Prover и Polyspace Code Prover Server могут помочь в идентификации недостижимого (и, следовательно, непроверяемого) кода, включая либо написанный вручную код, либо код, сгенерированный из модели.
С помощью набора DO Qualification Kit можно определить инспектора кода Simulink, поисковика ошибок Polyspace, сервера поиска ошибок Polyspace, программы проверки кода Polyspace и сервера проверки кода Polyspace.
Соответствие исходного кода стандартам можно проверить с помощью средства проверки правил MISRA C ®, MISRA ® C++ или JSF++ в программе поиска ошибок Polyspace, сервере поиска ошибок Polyspace, программе проверки кода Polyspace и сервере проверки кода Polyspace. Проверка MISRA C работает с Simulink. Эти продукты также способны определять цикломатическую сложность кода, который обычно также включается в стандарт кодирования.
С помощью квалификационного комплекта DO можно определить параметры Polyspace Bug Finder, Polyspace Bug Finder Server, Polyspace Code Prover и Polyspace Code Prover Server.
Прослеживаемость исходного кода до требований низкого уровня может быть проверена с помощью Simulink Code Inspector, который проверяет прослеживаемость между моделью и кодом и предоставляет отчет прослеживаемости.
Simulink Code Inspector может быть квалифицированным инструментом с помощью набора DO Qualification Kit.
Точность и непротиворечивость исходного кода можно проверить с помощью Simulink Code Inspector, который проверяет точность и непротиворечивость модели.
Polyspace Bug Finder, Polyspace Bug Finder Server, Polyspace Code Prover и Polyspace Code Prover Server могут определять ошибки времени выполнения, такие как потенциальное недозаполнение, переполнение, деление на ноль и т.д. Эти продукты также могут обнаруживать неинициализированные переменные и константы. В следующей таблице указаны действия для определения правильности и непротиворечивости исходного кода, а также того, охватываются ли эти действия продуктами Polyspace.
| Деятельность | Покрывается сервером Polyspace Bug Finder/Polyspace Bug Finder | Покрывается сервером проверки кода Polyspace/Polyspace Code Prover |
|---|---|---|
| Использование стека | Нет | Да |
| Использование памяти | Нет | Нет |
| Арифметическое переполнение с фиксированной точкой и разрешение | Да | Да |
| Арифметика с плавающей запятой | Да | Да |
| Соперничество и ограничения ресурсов | Нет | Нет |
| Наихудшее время выполнения | Нет | Нет |
| Обработка исключений | Нет | Нет |
| Использование неинициализированных переменных | Да | Да |
| Управление кэшем | Нет | Нет |
| Неиспользуемые переменные | Нет | Да |
| Повреждение данных из-за конфликтов задач или прерываний | Нет | Да |
Polyspace Bug Finder, Polyspace Bug Finder Server, Polyspace Code Prover и Polyspace Code Prover Server помогают идентифицировать:
Арифметические переполнения с фиксированной точкой
Использование неинициализированных переменных
Использование неинициализированных констант
Повреждение данных из-за конфликтов задач или прерываний
Неиспользуемые переменные
Неиспользуемые константы
Проблемы непротиворечивости типов
Преобразования типов, приводящие к недоливу или переполнению
Метрика использования стека
Эти продукты можно квалифицировать с помощью набора DO Qualification Kit.
Поскольку процесс интеграции не входит в область проектирования на основе модели, процесс интеграции можно проверить с помощью традиционных методов.
Поскольку процесс проверки файла элемента данных параметра не входит в область проектирования на основе модели, проверьте файл элемента данных параметра с помощью традиционных методов.
Поскольку процесс проверки файла элемента данных параметра не входит в область проектирования на основе модели, проверьте файл элемента данных параметра с помощью традиционных методов.
Это видно из квалификации Polyspace Code Prover и обоснования абстрактного толкования.
Это достигается путем просмотра отчета о результатах ошибок выполнения программы Polyspace Code Prover. Любые расхождения должны быть объяснены и обоснованы.
Это видно из квалификации Polyspace Code Prover и обоснования абстрактного толкования.
Теоретическая основа DO Qualification Kit: Polyspace Code Prover обосновывает обоснованность метода абстрактной интерпретации, используемого Polyspace Code Prover.