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