Следующая таблица содержит сводные данные верификации целей процесса кодирования и интегрирования на основе DO-178C, DO-331, DO-332 и DO-333, включая цели, применимые справочные разделы и уровни программного обеспечения, применимые к цели. Таблица также описывает доступные инструменты Модельно-ориентированное проектирование для достижения целей.
Таблица A-5: Верификация процесса кодирования и интегрирования
| Цель | Справочные разделы | Справочные разделы по действиям | Уровни программного обеспечения | Доступные продукты для Модельно-ориентированного проектирования | |
|---|---|---|---|---|---|
| 1 | Исходный код соответствует низкоуровневым требованиям. | MB.6.3.4.a | MB.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 | 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 Qualification Kit |
| 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 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 | MB.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 | MB.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 | 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 | Достигается верификация параметра Data Item File. | 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.
Верифицируемость кода может быть проверена с помощью 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 Theoretical Foundation обосновывает обоснованность метода абстрактной интерпретации, используемого Polyspace Code Prover.
