Следующая таблица содержит сводные данные верификации целей результатов процесса проверки от DO - 178C, DO-331, и DO-333 включая объективные, применимые ссылочные разделы и программных уровней, применимых к цели. Таблица также описывает доступные инструменты Model-Based Design, которые могут использоваться в удовлетворении целям.
Таблица 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 Мбит 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 | Мбит 6.8.3.2 | A, B, C | Не применяется (Кредит симуляции на тестирование EOC не взят), |
| МБАЙТ 11 | Процедуры симуляции правильны | MB.6.8.3.2.b | Мбит 6.8.3.2 | A, B, C | Не применяется (Кредит симуляции на тестирование EOC не взят), |
| МБАЙТ 12 | Результаты симуляции правильны и объясненные несоответствия | MB.6.8.3.2.c | Мбит 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 (Процессор в цикле) в Simulink, затем менеджер по Тесту в 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 Теоретическая Основа выравнивает по ширине разумность метода Абстрактной интерпретации, используемого Polyspace Code Prover и Polyspace Code Prover Server.
