В следующей таблице содержится резюме целей проверки результатов процесса проверки, полученных от DO-178C, DO-331 и DO-333, включая цель, применимые справочные разделы и уровни программного обеспечения, применимые к цели. В таблице также описаны доступные инструменты конструирования на основе модели, которые можно использовать для достижения поставленных целей.
Таблица A-7: Проверка результатов процесса проверки
| Цель | Справочные разделы | Справочные разделы по деятельности | Уровни программного обеспечения | Доступные продукты для конструирования на основе моделей | |
|---|---|---|---|---|---|
| 1 | Процедуры тестирования верны. | 6.4.5.b | 6.4.5 | A, B, C | Комплект для сертификации Simulink ® Coverage™, DO |
| 2 | Результаты испытаний верны, а расхождения объяснены. | 6.4.5.c | 6.4.5 | A, B, C | Simulink Test™, квалификационный комплект DO |
| 3 | Достигается тестовый охват высокоуровневых требований. | 6.4.4.a | 6.4.4.1 MB.6.8.2.a | A, B, C, D | Simulink Requirements™, квалификационный комплект DO |
| 4 | Достигается тестовый охват низкоуровневых требований. | 6.4.4.b | 6.4.4.1 MB.6.7 | A, B, C | Покрытие Simulink, квалификационный комплект DO |
| 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, квалификационный комплект DO |
| 6 | Достигается тестовый охват структуры программного обеспечения (покрытие принятия решений). | 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, квалификационный комплект DO |
| 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, квалификационный комплект DO |
| 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 |
| FM 2 | Результаты формального анализа верны, а расхождения объяснены | Из 6.7.2.c | ИЗ 6.7.2 | A, B, C | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
| 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, сервер проверки кода Polyspace, квалификационный комплект DO |
| FM 9 | Проверка сохранности свойств между исходным кодом и кодом объекта | Из 6.7.f | ИЗ 6.7 | A, B, C, D | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
| FM 10 | Формальный метод правильно определен, обоснован и уместен | ИЗ 6.2.1 | Из 6.2.1.a Из 6.2.1.b Из 6.2.1.c | A, B, C, D | Сервер проверки кода Polyspace, сервер проверки кода Polyspace, квалификационный комплект DO |
В следующих разделах более подробно описываются потенциальные последствия для каждой цели проверки результатов процесса проверки при использовании модели на основе конструкции, если это применимо, по сравнению с традиционной разработкой.
Правильность процедур испытаний из требований более высокого уровня может быть проверена путем анализа процедур испытаний. Во время моделирования покрытие модели проверяет, что условия и решения в модели были выполнены, и предоставляет полученные диапазоны данных. Адекватность диапазонов данных и ожидаемых результатов не проверяется по охвату модели. Отчет о покрытии модели может использоваться для проверки достоверности и полноты тестовых примеров, генерируемых Simulink Design Verifier™.
Полноту тестовых примеров, генерируемых Simulink Design Verifier, можно проверить путем выполнения тестовых примеров на модели Simulink при измерении охвата модели во время моделирования. Ожидаемые результаты, полученные Simulink, можно проверить путем просмотра результатов.
Возможность покрытия в Simulink Coverage может быть квалифицирована как средство проверки с помощью набора DO Qualification Kit.
Правильность результатов теста можно проверить, просмотрев результаты теста. Если используется Simulink Test совместно с режимом PIL (Processor in-the-loop) в Simulink, то для проверки результатов можно использовать Test Manager в Simulink Test. В качестве альтернативы, разработайте платформу тестирования процессора в цикле для исполняемого объектного кода, который может быть квалифицирован как средство проверки, чтобы определить состояние прохождения и неуспешности результатов.
Тестовый охват требований к высокоуровневому программному обеспечению может быть проверен путем анализа тестовых примеров и отслеживания соответствия высокоуровневым требованиям. Simulink Requirements можно использовать для отслеживания тестовых случаев в соответствии с высокоуровневыми требованиями, обеспечивая возможность проверки наличия соответствующих тестовых примеров в каждом требовании.
Тестовый охват требований к низкоуровневому программному обеспечению может быть проверен с помощью отчета о покрытии модели Simulink Coverage во время выполнения тестов на основе высокоуровневых требований. Отчет о покрытии модели предоставляет данные, помогающие доказать, что требования низкого уровня полностью удовлетворяются в ходе тестирования высокого уровня.
Возможность покрытия модели в Simulink Coverage может быть квалифицирована как средство проверки с помощью набора DO Qualification Kit.
Измененное состояние и покрытие принятия решений структуры программного обеспечения может быть проверено с использованием покрытия кода Simulink Coverage. Этот анализ выполняется во время выполнения тестов на основе требований, описанных в разделе Код исполняемого объекта соответствует высокоуровневым требованиям.
Если основанные на требованиях тестовые примеры разрабатываются на уровне модели и повторно используются для тестирования исполняемого объектного кода, возможность покрытия модели Simulink Coverage может использоваться во время разработки основанных на требованиях тестовых примеров. Использование этой возможности помогает прогнозировать эффективность тестовых случаев в обеспечении структурного покрытия генерируемого кода.
Возможность покрытия кода в Simulink Coverage может быть квалифицирована как средство проверки с помощью набора DO Qualification Kit.
Покрытие решения структуры программного обеспечения может быть проверено с использованием покрытия кода Simulink Coverage. Этот анализ выполняется во время выполнения тестов на основе требований, описанных в разделе Код исполняемого объекта соответствует высокоуровневым требованиям.
Если основанные на требованиях тестовые примеры разработаны на уровне модели и повторно используются для тестирования исполняемого кода объекта, то возможность покрытия модели может быть использована во время разработки основанных на требованиях тестовых примеров. Использование инструмента помогает прогнозировать эффективность тестовых случаев в обеспечении структурного покрытия для сгенерированного кода.
Возможность покрытия кода в Simulink Coverage может быть квалифицирована как средство проверки с помощью набора DO Qualification Kit.
Покрытие инструкций структуры программного обеспечения может быть проверено с использованием покрытия кода Simulink Coverage. Этот анализ выполняется во время выполнения тестов на основе требований, описанных в разделе Код исполняемого объекта соответствует высокоуровневым требованиям.
Если основанные на требованиях тестовые примеры разрабатываются на уровне модели и повторно используются для тестирования исполняемого кода объекта, то возможность покрытия модели может быть использована во время разработки основанных на требованиях тестовых примеров. Использование инструмента помогает прогнозировать эффективность тестовых случаев в обеспечении структурного покрытия для сгенерированного кода.
Возможность покрытия кода в Simulink Coverage может быть квалифицирована как средство проверки с помощью набора DO Qualification Kit.
Поскольку соединение данных и управление не входят в объем кода, генерируемого с помощью конструкции на основе модели, соединение данных и управление данными можно проверить с помощью традиционных методов. Тестовый охват для связи и управления данными включает в себя проверку интерфейсов данных к и от автоматически генерируемого кода и последовательности вызова автоматически генерируемого кода относительно других модулей кода.
Поскольку дополнительный процесс проверки объектного кода не входит в область проектирования на основе модели, проверьте дополнительный объектный код с помощью традиционных методов. Однако образец модели элементов Simulink и Stateflow ®, используемый проектом, может использоваться для создания кода, который предоставляет образец исходного кода для оценки прослеживаемости объектного кода.
Этот объект применим только в том случае, если для моделирования вместо тестирования исполняемого кода объекта используется кредит. Это не рекомендуется из-за сложности демонстрации эквивалентности между моделированием на основе хоста и целевым кодом.
Этот объект применим только в том случае, если для моделирования вместо тестирования исполняемого кода объекта используется кредит. Это не рекомендуется из-за сложности демонстрации эквивалентности между моделированием на основе хоста и целевым кодом.
Этот объект применим только в том случае, если для моделирования вместо тестирования исполняемого кода объекта используется кредит. Это не рекомендуется из-за сложности демонстрации эквивалентности между моделированием на основе хоста и целевым кодом.
Это показано с помощью квалификации Polyspace Code Prover и Polyspace Code Prover Server и обоснования абстрактной интерпретации.
Это достигается путем просмотра отчета о результатах ошибок выполнения сервера проверки кода Polyspace и сервера проверки кода 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 не поддерживают эту цель.
Polyspace Code Prover и Polyspace Code Prover Server могут использоваться для поиска недостижимого кода, независимо от того, написан он вручную или сгенерирован из модели. Задачи структурного покрытия и связи данных и контроля покрытия все еще должны быть достигнуты в ходе тестирования, как описано в предыдущих разделах.
Анализ сервера проверки кода Polyspace и сервера проверки кода Polyspace используется только для определения определенных типов ошибок. Тестирование исполняемого объектного кода на соответствие требованиям высокого и низкого уровня по-прежнему необходимо для полного удовлетворения целей исполняемого объектного кода. Чтобы продемонстрировать сохранение свойств между исходным и объектным кодом, необходимо выполнить анализ прослеживаемости между исходным и объектным кодом, чтобы продемонстрировать, что дополнительный код, не отслеживаемый непосредственно с исходным кодом, не вставляется. Кроме того, тесты могут использоваться, чтобы показать, что свойства сохраняются между низкоуровневыми требованиями, исходным кодом и исполняемым объектным кодом.
Теоретическая основа DO Qualification Kit: Polyspace Code Prover обосновывает обоснованность метода Abstract Interpretation, используемого сервером Polyspace Code Prover и сервером Polyspace Code Prover.