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