Следующая таблица содержит сводные данные верификации целей кодирования и процесса интеграции от 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 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.
Соответствие стандартов исходного кода может быть проверено с помощью 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.
