Следующая таблица содержит сводные данные результатов верификации результатов процесса проверки по DO-178C, DO-331 и DO-333, включая целевые, применимые справочные разделы и уровни программного обеспечения, применимые к цели. Таблица также описывает доступные инструменты Модельно-ориентированное проектирование, которые могут использоваться для достижения целей.
Таблица A-7: Проверка результатов процесса верификации
| Цель | Справочные разделы | Справочные разделы по действиям | Уровни программного обеспечения | Доступные продукты для Модельно-ориентированного проектирования | |
|---|---|---|---|---|---|
| 1 | Процедуры тестирования верны. | 6.4.5.b | 6.4.5 | A, B, C | Simulink® Coverage™, DO Qualification Kit |
| 2 | Результаты теста верны и объяснены расхождения. | 6.4.5.c | 6.4.5 | A, B, C | Simulink Test™, DO Qualification Kit |
| 3 | Обеспечивается тестовое покрытие требований высокого уровня. | 6.4.4.a | 6.4.4.1 MB.6.8.2.a | A, B, C, D | Simulink Requirements™, DO Qualification Kit |
| 4 | Обеспечивается тестовое покрытие низкоуровневых требований. | 6.4.4.b | 6.4.4.1 MB.6.7 | A, B, C | Simulink Coverage, DO Qualification Kit |
| 5 | Тестовое покрытие структуры программного обеспечения (измененное состояние/решение) достигается. | 6.4.4.c | 6.4.4.2.a 6.4.4.2.b 6.4.4.2.d 6.4.4.3 MB.6.8.2.b | A | Simulink Coverage, DO Qualification Kit |
| 6 | Тестовое покрытие структуры ( Decision Coverage) программного обеспечения достигается. | 6.4.4.c | 6.4.4.2.a 6.4.4.2.b 6.4.4.2.d 6.4.4.3 MB.6.8.2.b | A, B | Simulink Coverage, DO Qualification Kit |
| 7 | Тестовое покрытие структуры программного обеспечения (покрытие оператора) достигается. | 6.4.4.c | 6.4.4.2.a 6.4.4.2.b 6.4.4.2.d 6.4.4.3 MB.6.8.2.b | A, B, C | Simulink Coverage, DO Qualification Kit |
| 8 | Тестовое покрытие структуры программного обеспечения (связь данных и муфта управления) достигается. | 6.4.4.d | 6.4.4.2.c 6.4.4.2.d 6.4.4.3 MB.6.8.2.b | A, B, C | Не применяется (Кредит симуляции для проверки EOC не взят) |
| 9 | Выполняется проверка дополнительного кода, который нельзя отследить до исходного кода. | 6.4.4.c | 6.4.4.2.b | A | Не применяется (Кредит симуляции для проверки EOC не взят) |
| МБ 10 | Случаи симуляции верны | MB.6.8.3.2.a | MB.6.8.3.2 | A, B, C | Не применяется (Кредит симуляции для проверки EOC не взят) |
| МБ 11 | Процедуры симуляции верны | MB.6.8.3.2.b | MB.6.8.3.2 | A, B, C | Не применяется (Кредит симуляции для проверки EOC не взят) |
| МБ 12 | Результаты симуляции верны и объяснены расхождения | MB.6.8.3.2.c | MB.6.8.3.2 | A, B, C | Не применяется (Кредит симуляции для проверки EOC не взят) |
| FM 1 | Формальные случаи анализа и процедуры верны | Из 6.7.2.a Из 6.7.2.b | ИЗ 6.7.2 | A, B, C | Polyspace® Code Prover™, Polyspace Code Prover Server™, DO Qualification Kit |
| FM 2 | Формальные результаты анализа верны и объяснены расхождения | Из 6.7.2.c | ИЗ 6.7.2 | A, B, C | Polyspace Code Prover, Polyspace Code Prover Server, DO Qualification Kit |
| FM 3 | Охват требований высокого уровня достигается | Из 6.7.1.a | ИЗ 6.7.1.1 | A, B, C, D | Неприменимо |
| FM 4 | Обеспечивается удовлетворение низкоуровневых потребностей | Из 6.7.1.a | ИЗ 6.7.1.1 | A, B, C | Неприменимо |
| FM 5-8 | Обеспечивается верификационный охват структуры программного обеспечения | Из 6.7.1.c | ИЗ 6.7.1.2 ИЗ 6.7.1.3 ИЗ 6.7.1.4 ИЗ 6.7.1.5 | A, B, C | Polyspace Code Prover, Polyspace Code Prover Server, DO Qualification Kit |
| FM 9 | Верификация сохранения свойств между исходным и объектным кодом | Из 6.7.f | ИЗ 6.7 | A, B, C, D | Polyspace Code Prover, Polyspace Code Prover Server, DO Qualification Kit |
| FM 10 | Формальный метод правильно определен, обоснован и уместен | ИЗ 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 Design Verifier™.
Полнота тестов, сгенерированных Simulink Design Verifier, может быть проверена путем выполнения тестов на модели Simulink с измерением покрытия модели во время симуляции. Ожидаемые результаты, полученные Simulink, могут быть проверены путем просмотра результатов.
Возможность покрытия в Simulink Coverage может быть квалифицирована как инструмент верификации с помощью DO Qualification Kit.
Правильность результатов теста может быть проверена путем просмотра результатов тестирования. Если при использовании Simulink Test в сочетании с PIL-режимом (Processor in-the-loop) в Simulink, то для верификации результатов Pass/Fail может использоваться Test Manager в Simulink Test. В качестве альтернативы разработайте тестовую платформу процессора в цикле для исполняемого объектного кода, который может быть квалифицирован как инструмент верификации в порядок определения статуса прохождения и непрохождения результатов.
Охват тестами требований к программному обеспечению высокого уровня может быть проверен путем анализа тестовых примеров и трассируемости в соответствии с требованиями высокого уровня. Simulink Requirements может использоваться, чтобы проследить тесты до требований высокого уровня, предоставляя возможность помочь в проверке того, что каждое требование связано с тестами.
Покрытие тестов низкоуровневых требований к программному обеспечению может быть проверено с помощью отчета о покрытии модели Simulink Coverage во время выполнения основанных на требованиях тестов высокого уровня. В докладе о покрытии модели содержатся данные, которые помогают доказать, что низкоуровневые требования полностью удовлетворяются во время проверки высокого уровня.
Возможность покрытия модели в Simulink Coverage может быть квалифицирована как инструмент верификации с помощью DO Qualification Kit.
Измененное условие и Decision Coverage структуры программного обеспечения могут быть проверены с помощью покрытия кода Simulink Coverage. Этот анализ выполняется во время выполнения основанных на требованиях тестов, описанных в Исполняемом объектном коде Соответствует Требованиям высокого уровня.
Если основанные на требованиях тесты разрабатываются на уровне модели и повторно используются для проверки исполняемого объектного кода, возможность покрытия модели Simulink Coverage может использоваться во время разработки основанных на требованиях тестов. Использование возможности помогает предсказать эффективность тестов в обеспечении структурного покрытия для сгенерированного кода.
Возможность покрытия кода в Simulink Coverage может быть квалифицирована как инструмент верификации с помощью DO Qualification Kit.
Decision Coverage структуры программного обеспечения может быть проверено с помощью покрытия кода Simulink Coverage. Этот анализ выполняется во время выполнения основанных на требованиях тестов, описанных в Исполняемом объектном коде Соответствует Требованиям высокого уровня.
Если основанные на требованиях тесты разрабатываются на уровне модели и повторно используются для проверки из исполняемого объектного кода, возможность покрытия модели может использоваться во время разработки основанных на требованиях тестов. Использование инструмента помогает предсказать эффективность тестов в обеспечении структурного покрытия для сгенерированного кода.
Возможность покрытия кода в Simulink Coverage может быть квалифицирована как инструмент верификации с помощью DO Qualification Kit.
Покрытие операторов структуры программного обеспечения может быть проверено с помощью покрытия кода Simulink Coverage. Этот анализ выполняется во время выполнения основанных на требованиях тестов, описанных в Исполняемом объектном коде Соответствует Требованиям высокого уровня.
Если основанные на требованиях тесты разрабатываются на уровне модели и повторно используются для проверки из исполняемого объектного кода, то возможность покрытия модели может использоваться во время разработки основанных на требованиях тестов. Использование инструмента помогает предсказать эффективность тестов в обеспечении структурного покрытия для сгенерированного кода.
Возможность покрытия кода в Simulink Coverage может быть квалифицирована как инструмент верификации с помощью DO Qualification Kit.
Поскольку связывание данных и управление находятся вне возможностей кода, сгенерированного с помощью Модельно-ориентированное Проектирование, связывание данных и управление могут быть проверены с помощью традиционных методов. Тестовое покрытие для связи и управления данными включает в себя верификацию интерфейсов данных к автоматически сгенерированному коду и от него и последовательности вызовов автоматически сгенерированного кода относительно других модулей кода.
Поскольку дополнительный процесс проверки объектного кода находится вне возможностей Модельно-ориентированное Проектирование, проверьте дополнительный объектный код с помощью традиционных методов. Однако выборка модели Simulink и Stateflow® элементы, используемые проектом, могут использоваться для генерации кода, который предоставляет выборку исходного кода для оценки трассируемости объектного кода.
Этот объект применим только, когда кредит взят для симуляции вместо проверки исполняемого объектного кода. Это не рекомендуемый рабочий процесс из-за сложности демонстрации эквивалентности между симуляцией на основе хоста и целевым кодом.
Этот объект применим только, когда кредит взят для симуляции вместо проверки исполняемого объектного кода. Это не рекомендуемый рабочий процесс из-за сложности демонстрации эквивалентности между симуляцией на основе хоста и целевым кодом.
Этот объект применим только, когда кредит взят для симуляции вместо проверки исполняемого объектного кода. Это не рекомендуемый рабочий процесс из-за сложности демонстрации эквивалентности между симуляцией на основе хоста и целевым кодом.
Это показано через проверку Polyspace Code Prover и Polyspace Code Prover Server и обоснование абстрактной интерпретации.
Это достигается с помощью анализа отчета о результатах ошибки во время запуска Polyspace Code Prover и Polyspace Code Prover Server. Любые расхождения должны быть объяснены и обоснованы.
Не применяется, 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 не поддерживают эту цель.
Polyspace Code Prover и Polyspace Code Prover Server могут использоваться, чтобы найти недоступный код, написанный вручную или сгенерированный из модели. Цели структурного покрытия и связывания данных и контроля должны все еще достигаться во время проверки, как описано в предыдущих разделах.
Анализ Polyspace Code Prover и Polyspace Code Prover Server используется только для получения кредита на обнаружение определенных типов ошибок. Проверка исполняемого объектного кода на соответствие требованиям высокого и низкого уровня все еще требуется, чтобы полностью удовлетворить целям исполняемого исполняемого объектного кода. В порядок, чтобы продемонстрировать сохранение свойств между исходным и объектным кодом, необходимо выполнить анализ трассируемости между исходным и объектным кодами, чтобы продемонстрировать, что дополнительный код, не отслеживаемый непосредственно к исходному коду, не вставлен. Кроме того, тесты могут использоваться, чтобы показать, что свойства сохраняются между низкоуровневыми требованиями, исходным кодом и исполняемым объектным кодом.
DO Qualification Kit: Polyspace Code Prover Theoretical Foundation обосновывает обоснованность метода абстрактной интерпретации, используемого Polyspace Code Prover и Polyspace Code Prover Server.
