Следующая таблица содержит сводные данные проверки выходов целей интегрирования процесса из DO-178C и DO-333, включая целевые, применимые разделы ссылки и уровни программного обеспечения, применимые к цели. Таблица также описывает доступные инструменты Модельно-ориентированное проектирование для достижения целей.
Таблица A-6: Проверка выходов Интегрирования процесса
| Цель | Справочные разделы | Справочные разделы по действиям | Уровни программного обеспечения | Доступные продукты для Модельно-ориентированного проектирования | |
|---|---|---|---|---|---|
| 1 | Исполняемый объектный код соответствует требованиям высокого уровня. | 6.4.a | 6.4.2 6.4.2.1 6.4.3 6.5 | A, B, C, D | Simulink® Test™, Simulink Design Verifier™, Embedded Coder® - PIL Mode, DO Qualification Kit |
| 2 | Исполняемый объектный код является надежным с требованиями высокого уровня. | 6.4.b Из 6.7.b Из 6.7.c | 6.4.2 6.4.2.2 6.4.3 6.5 ИЗ 6.7 ИЗ 6.5 | A, B, C, D | Simulink Test, Simulink Design Verifier, Embedded Coder - PIL Mode, Polyspace® Code Prover™, Polyspace Code Prover Server™, DO Qualification Kit |
| 3 | Исполняемый объектный код соответствует низкоуровневым требованиям. | 6.4. | 6.4.2 6.4.2.1 6.4.3 6.5 | A, B, C | Simulink Test, Simulink Design Verifier, Embedded Coder - PIL Mode, DO Qualification Kit |
| 4 | Исполняемый объектный код является надежным с низкоуровневыми требованиями. | 6.4.d Из 6.7.b Из 6.7.c | 6.4.2 6.4.2.2 6.4.3 6.5 ИЗ 6.7 ИЗ 6.5 | A, B, C | Simulink Test, Simulink Design Verifier, Embedded Coder - PIL Mode, Polyspace Code Prover, Polyspace Code Prover Server, DO Qualification Kit |
| 5 | Исполняемый объектный код совместим с целевым компьютером. | 6.4.e | 6.4.1.a 6.4.3.a | A, B, C, D | Embedded Coder - режим PIL |
В следующих разделах более подробно описываются потенциальные воздействия для каждого тестирования выходных параметров интеграционного процесса при использовании основанного на модели проекта, если применимо, по сравнению с традиционной разработкой.
Можно проверить исполняемый объектный код, повторно используя те же тесты, которые используются для проверки моделей. Во время выполнения тестов верификации модели, с помощью Simulink Test, входы и выходы каждой тестируемой модели могут быть записаны и сохранены для использования при проверке исполняемого объектного кода.
В случае, когда модель спецификации существует, Simulink Design Verifier может использоваться, чтобы сгенерировать тесты высокого уровня из модели спецификации. Эти тесты могут быть запущены на Модель Проекта и исполняемом объектном коде, а также результаты по сравнению с ожидаемыми результатами модели спецификации. Сравнение используется, чтобы продемонстрировать, что исполняемый объектный код соответствует требованиям высокого уровня.
Исполняемый объектный код может быть протестирован на целевом процессоре или DSP с помощью функции PIL Mode Embedded Coder. Simulink Test может использоваться, чтобы выполнить эти тесты и сравнить результаты тестирования с ожидаемыми результатами.
При использовании для определения прохождения и непрохождения, менеджер тестирования в Simulink Test может быть квалифицирован как инструмент верификации с помощью DO Qualification Kit.
Тесты робастности должны быть разработаны против моделей и могут быть проведены с помощью Simulink Test.Робастность исполняемого объектного кода может быть проверена путем переиспользования тех же тестовых примеров, которые используются для проверки робастности моделей. Во время выполнения тестов верификации модели, с помощью Simulink Test, входы и выходы каждой тестируемой модели могут быть записаны и сохранены для использования при проверке исполняемого объектного кода.
В случае, когда модель спецификации существует, Simulink Design Verifier может использоваться, чтобы сгенерировать тесты робастности из модели спецификации. Эти тесты могут быть запущены на Модель Проекта и исполняемом объектном коде, а также результаты по сравнению с ожидаемыми результатами модели спецификации. Сравнение демонстрирует, что исполняемый объектный код надежен с требованиями высокого уровня. Для тестов робастности могут использоваться блоки Test Condition и Цель Тестирования, чтобы помочь в определении тестов, которые выполняют объектный код за пределами нормальных граничных условий.
Исполняемый объектный код может быть протестирован на целевом процессоре или DSP с помощью функции PIL Mode Embedded Coder. Simulink Test может использоваться, чтобы выполнить эти тесты и сравнить результаты тестирования с ожидаемыми результатами.
При использовании для определения прохождения и непрохождения, менеджер тестов в Simulink Test может быть квалифицирован как инструмент верификации с помощью DO Qualification Kit.
Можно также использовать Polyspace Code Prover и Polyspace Code Prover Server, чтобы удовлетворить эту цель путем проверки исходного кода с помощью абстрактной интерпретации. Некоторые ошибки, обнаруженные Polyspace Code Prover или Polyspace Code Prover Server, могут не быть обнаружены во время традиционной динамической проверки.
В следующей таблице определены действия для случаев робастности и может ли Polyspace Code Prover или Polyspace Code Prover Server использоваться, чтобы продемонстрировать способность программного обеспечения реагировать на ненормальные входы и условия согласно целевым FM.6.7.b.
| Деятельность | Покрывается Polyspace Code Prover/Polyspace Code Prover Server |
|---|---|
| Следует учитывать вещественные и целочисленные переменные. | Да |
| Инициализация системы должна учитываться в ненормальных условиях. | Нет |
| Должны быть определены возможные типы отказа входящих данных, особенно сложных, цифровых строк данных от внешней системы. | Нет |
| Для циклов, где количество циклов является вычисленным значением, должны быть разработаны формальные случаи анализа, чтобы попытаться вычислить значения количества циклов вне области допустимого, и, таким образом, продемонстрировать робастность кода, связанного с циклом. | Да |
| Должна быть проведена проверка, чтобы убедиться, что механизмы защиты для превышенного времени системы координат реагируют правильно. | Нет |
| Для связанных со временем функций, таких как фильтры, интеграторы и задержки, должен быть разработан формальный случай анализа для механизмов арифметического переполнения. | Да |
| Для переходов в состоянии должны быть разработаны формальные случаи анализа, чтобы спровоцировать переходы, которые не допускаются требованиями программного обеспечения. | Да |
Что касается объективных FM.6.7.b, Polyspace Code Prover и Polyspace Code Prover Server помогают идентифицировать:
Обнаружение арифметических дефектов
Обнаружение нарушений пределов массива
Обнаружение переполнений
Обнаружение циклов, приводящих к ошибке времени выполнения
Обнаружение неправильного логического решения, приводящего к недоступному коду или ошибкам времени выполнения
Цель FM.6.7.c заключается в верификации целостности программного обеспечения, чтобы обеспечить правильное взаимодействие компонентов программного обеспечения друг с другом и удовлетворить требования к программному обеспечению и программной архитектуре. В следующей таблице определены типичные ошибки, и принимает ли их во факторе Polyspace Code Prover и Polyspace Code Prover Server.
| Деятельность | Покрывается Polyspace Code Prover/Polyspace Code Prover Server |
|---|---|
| Неправильная инициализация переменных и констант | Да |
| Ошибки при передаче параметра. | Да |
| Повреждение данных, особенно глобальных данных. | Да |
| Неадекватное сквозное числовое разрешение. | Да |
| Неправильное секвенирование событий и операций. | Да |
Что касается объективных FM.6.7.c, Polyspace Code Prover и Polyspace Code Prover Server помогают идентифицировать:
Неинициализированные переменные
Ошибки передачи параметра
Повреждение данных, особенно глобальных данных
Неправильная инициализация переменных и констант
Неправильная инициализация переменных и констант, приводящих к недействию/переполнению
Глобальные данные общих переменных без механизма защиты
Неправильное секвенирование событий и операций
Polyspace Code Prover можно квалифицировать как инструмент верификации с помощью DO Qualification Kit.
Simulink Design Verifier может использоваться, чтобы сгенерировать низкоуровневые тесты из модели. Эти тесты могут быть запущены на модели и исполняемом объектном коде, и результаты сравнения. Сравнение используется, чтобы продемонстрировать, что исполняемый объектный код соответствует низкоуровневым требованиям.
Исполняемый объектный код может быть протестирован на целевом процессоре или DSP с помощью функции PIL Mode Embedded Coder. Simulink Test может использоваться, чтобы выполнить эти тесты и сравнить результаты тестирования с ожидаемыми результатами.
При использовании для определения прохождения и непрохождения, менеджер тестов в Simulink Test может быть квалифицирован как инструмент верификации с помощью DO Qualification Kit.
Кроме того, верификации с низкоуровневыми требованиями могут быть устранены, если основанные на требованиях покрытие и структурное покрытие достигаются с помощью основанных на высоких требованиях тестов (для примера, программного обеспечения интегрирования тестов). В разделе 6.4 DO-178C приведены следующие указания:
| Если контрольный пример и соответствующая ему процедура тестирования разрабатываются и выполняются для аппаратной / программной интеграционной проверки или интеграционной проверки программного обеспечения и удовлетворяют основанному на требованиях покрытию и структурному покрытию, нет необходимости дублировать тест для низкоуровневой проверки. Подстановка номинально эквивалентных низкоуровневых тестов для высокоуровневых тестов может быть менее эффективной из-за меньшего количества протестированной общей функциональности. |
Simulink Design Verifier может использоваться, чтобы сгенерировать тесты робастности из модели. Эти тесты могут быть запущены на модели и исполняемом объектном коде, и результаты сравнения. Сравнение показывает, что исполняемый объектный код является устойчивым с низкоуровневыми требованиями. Для тестов робастности Test Condition и Test Objective блоки могут использоваться, чтобы помочь в определении тестов, которые используют объектный код вне нормальных граничных условий.
Исполняемый объектный код может быть протестирован на целевом процессоре или DSP с помощью функции PIL Mode Embedded Coder. Simulink Test может использоваться, чтобы выполнить эти тесты и сравнить результаты тестирования с ожидаемыми результатами.
При использовании для определения прохождения и непрохождения, менеджер тестов в Simulink Test может быть квалифицирован как инструмент верификации с помощью DO Qualification Kit.
Polyspace Code Prover также может использоваться, чтобы удовлетворить этой цели, проверяя исходный код с помощью абстрактной интерпретации. Некоторые ошибки, обнаруженные Polyspace Code Prover и Polyspace Code Prover Server, могут не быть обнаружены во время традиционной динамической проверки.
В следующей таблице определены действия для случаев робастности и может ли Polyspace Code Prover и Polyspace Code Prover Server использоваться, чтобы продемонстрировать способность программного обеспечения реагировать на ненормальные входы и условия согласно целевым FM.6.7.b.
| Деятельность | Покрывается Polyspace Code Prover/Polyspace Code Prover Server |
|---|---|
| Следует учитывать вещественные и целочисленные переменные. | Да |
| Инициализация системы должна учитываться в ненормальных условиях. | Нет |
| Должны быть определены возможные типы отказа входящих данных, особенно сложных, цифровых строк данных от внешней системы. | Нет |
| Для циклов, где количество циклов является вычисленным значением, должны быть разработаны формальные случаи анализа, чтобы попытаться вычислить значения количества циклов вне области допустимого, и, таким образом, продемонстрировать робастность кода, связанного с циклом. | Да |
| Должна быть проведена проверка, чтобы убедиться, что механизмы защиты для превышенного времени системы координат реагируют правильно. | Нет |
| Для связанных со временем функций, таких как фильтры, интеграторы и задержки, должен быть разработан формальный случай анализа для механизмов арифметического переполнения. | Да |
| Для переходов в состоянии должны быть разработаны формальные случаи анализа, чтобы спровоцировать переходы, которые не допускаются требованиями программного обеспечения. | Да |
Что касается объективных FM.6.7.b, Polyspace Code Prover и Polyspace Code Prover Server помогают идентифицировать:
Обнаружение арифметических дефектов
Обнаружение нарушений пределов массива
Обнаружение переполнений
Обнаружение циклов, приводящих к ошибке времени выполнения
Обнаружение неправильного логического решения, приводящего к недоступному коду или ошибкам времени выполнения
Цель FM.6.7.c заключается в верификации целостности программного обеспечения, чтобы обеспечить правильное взаимодействие компонентов программного обеспечения друг с другом и соответствие требованиям к программному обеспечению и программной архитектуре. В следующей таблице определены типичные ошибки, и принимает ли их во факторе Polyspace Code Prover и Polyspace Code Prover Server.
| Деятельность | Покрывается Polyspace Code Prover/Polyspace Code Prover Server |
|---|---|
| Неправильная инициализация переменных и констант | Да |
| Ошибки при передаче параметра. | Да |
| Повреждение данных, особенно глобальных данных. | Да |
| Неадекватное сквозное числовое разрешение. | Да |
| Неправильное секвенирование событий и операций. | Да |
Что касается объективных FM.6.7.c, Polyspace Code Prover помогает идентифицировать:
Неинициализированные переменные
Ошибки передачи параметра
Повреждение данных, особенно глобальных данных
Неправильная инициализация переменных и констант
Неправильная инициализация переменных и констант, приводящих к недействию/переполнению
Глобальные данные общих переменных без механизма защиты
Неправильное секвенирование событий и операций
Polyspace Code Prover можно квалифицировать как инструмент верификации с помощью DO Qualification Kit.
Можно оценить исполняемый объектный код на использование стека, использование памяти и время выполнения на целевом процессоре или DSP, используя возможность Embedded Coder PIL Mode.
Другие аспекты совместимости оборудования, такие как обработка прерываний, конкуренция ресурсов, оборудования интерфейсы, секционирование и т.д., должны быть проверены с помощью традиционных методов.
