Efficient Verification of Safe Avionics Software with DO-178C Objectives Using SCADE Suite

May 19, 2025 at 2:26 pm

Solution

Participant

This article is part of a DO-178C blog series. It gives an overview of the DO-178C avionics software standard and details the process of developing, then verifying, safe compliant applications. You can find links to each part below:

Part 1: An introduction to DO-178C
Part 2: Efficient Development of Safe Avionics Software with DO-178C Objectives Using SCADE Suite
Part 3 (this blog): Efficient Verification of Safe Avionics Software with DO-178C Objectives Using SCADE Suite

In our previous blog, we explored how to fully meet DO-178C development objectives using the SCADE Suite model-based approach for avionics software development.

In this post, we’ll delve into the Verification aspect of DO-178C, demonstrating how SCADE supports an efficient verification strategy that reduces costs and boosts productivity.

Model-Based Development with SCADE

SCADE Suite is a robust software design solution specifically crafted for modeling, verifying, and generating code for embedded control systems. It provides a user-friendly, intuitive, and model-based development environment, enabling software engineers to streamline and optimize their workflows.

SCADE Suite offers the following key highlights:

Embedded Control Software Design: streamlined development of control systems, logic, and algorithms within an integrated environment. Seamlessly integrates data flow and state machine operators, providing unmatched flexibility and precision across all design levels.
Integrated Suite for Prototyping, Modeling, Simulation, Verification and Optimization: efficient debugging and optimization of software models and code size, speed, and performance.
Safe Code Generation: automatic C and Ada qualified code generators (DO-178C/DO-330, EN 50128, ISO 26262, IEC 61508) also the basis for testing cost reduction.

Model-based software design with qualified code generation

SCADE Suite seamlessly integrates with SCADE Test, offering engineers a comprehensive testing environment for both SCADE Suite and SCADE Display models. SCADE Test enables the creation and management of test cases, execution of tests on both host and target systems, and assessment of model coverage. It provides a user-friendly, intuitive environment specifically designed for verification engineers.

Software Verification Activities with SCADE Suite & SCADE Test

When using a model-based approach with qualified code generation, the software verification activities are adapted to include model-based specific techniques. The main changes are the activities performed at model level:

Model Review: similar to code reviews, model reviews involve examining the model to ensure it accurately represents the software requirements and architecture.
Model Simulation: this involves executing the model to verify its behavior against expected outcomes.
Model Coverage Analysis: ensuring that all parts of the model have been exercised during simulation to identify any untested sections.

The other activities do not have much difference between a model approach or manual code.

Let’s review the main activities.

Verification of High-Level Requirements‌

In a typical SCADE Suite development process, the high-level requirements (HLR) are usually in textual form and include functional, performance, interface and safety-related requirements.

These requirements must be verified against the objectives of DO-178C Table A-3. Due to their textual form, this compliance is mainly addressed in a traditional way by peer review.

The following table (DO-178C Table A-3) lists the verification objectives for the software high-level requirements.

Objective Description	Objective Ref	Activity Ref	Verification Method
1. High-level requirements comply with system requirements	MB.6.3.1.a	6.3.1	Peer review
2. High-level requirements are accurate and consistent	MB.6.3.1.b	6.3.1	Peer review
3. High-level requirements are compatible with target computer	MB.6.3.1.c	6.3.1	Peer review
4. High-level requirements are verifiable	MB.6.3.1.d	6.3.1	Peer review
5. High-level requirements conform to standards	MB.6.3.1.e	6.3.1	Peer review
6. High-level requirements are traceable to system requirements	MB.6.3.1.f	6.3.1	Peer review
7. Algorithms are accurate	MB.6.3.1.g	6.3.1	Peer review

Verification of the model and the software architecture

The SCADE Suite design models have to be verified against the objectives of DO-331 Table MB.A-4. The following verification methods should be used:

Verification of the SCADE model. Peer review to ensure that the SCADE model (positioned as LLRs) complies with the HLRs, using the HLR/SCADE model traceability matrix (built with SCADE ALM Gateway) and the model report (generated by SCADE LifeCycle Reporter).
Development of HLR-based verification cases and procedures from the requirements from which the SCADE model was developed. Verification cases and procedures shall address the same considerations as those for normal range and robustness test cases and procedures and possible error sources (see [DO-178C] 6.4.2). The test cases and procedures are developed using SCADE Test.
Verification of HLR-based verification cases and procedures. Peer review of SCADE verification cases and procedures to confirm that they are traceable to HLRs, that they satisfy criteria of normal and robustness testing and that all HLRs are covered by verification cases (see objectives MB.14 and MB.15).
Model simulation allows exercising the behavior of the model. DO-331 provides a precise definition and some specific guidance in §MB.6.8: Model Simulation is defined as “The activity of exercising the behavior of a model using a model simulator“. As stated in DO-331, MB.6.8.1, its main purpose is to provide repeatable evidence of compliance of the model to the requirements from which the model was developed. Moreover, model simulation is an efficient way to detect functional issues very early in the software design and/or upper-level requirements. Model simulation is performed on the development platform using the HLR-based verification cases and procedures and SCADE Test Environment for Host.
Verification of Model simulation results. SCADE simulation results are reviewed to confirm that they are complete and correct, and all deficiencies are explained (see objective MB.16).
Model coverage analysis assesses how thoroughly the SCADE model is exercised during model simulation using the HLR-based verification cases and procedures. It helps assess the completeness of model testing and ensures that all model components behave as expected. Model coverage analysis contributes to the detection and resolution of shortcomings in the verification cases or procedures, inadequacies or shortcomings in requirements, and deactivated or unintended functionality expressed by the design model. Model coverage is performed using SCADE Test Model Coverage.
Syntactic and semantic checks using SCADE Suite KCG Semantics Checker. This checker verifies that the model follow the rules of the Scade language syntax and semantics (such as type and clock consistency, initialization of data flows, or causality in models)
CVK. While SCADE Suite KCG qualification ensures that generated code conforms to the model, CVK is a test suite that can be used to verify that the type of code generated by SCADE Suite KCG is correctly compiled/executed with a given cross-compiler on a given target. CVK can be used for the following purposes:
- to support early verification of the correctness and consistency between the development tool chain and the target platform
- to address the verification of target
Verifying modeling guidelines and model complexity. This verification can be done either automatically or manually. In the context of automatic verification, users are able to develop their own design rules by using SCADE Suite Metrics and Rules Checker scripting capabilities. This tool is not qualified: qualification must be done by the user for ones’ specific rules.

The following table (DO-331 Table MB.A-4) summarizes verification objectives and methods for the software low-level requirements and architecture.

Objective Description	Objective Ref	Activity Ref	Verification Method
1. Low-level requirements comply with high-level requirements	MB.6.3.2.a	MB.6.3.2 MB.6.7 MB.6.8.1 (see Item 1)	Peer review with SCADE LifeCycle Reporter Development of HLR-based SCADE verification cases and procedures with SCADE Test Model simulation with SCADE Test Model coverage analysis with SCADE Model Coverage
2. Low-level requirements are accurate and consistent	MB.6.3.2.b	MB.6.3.2 MB.6.8.1 (see Item 1)	Syntactic and semantic checks automated with SCADE Suite KCG Semantics Checker Peer review with SCADE LifeCycle Reporter Review of SCADE Model Coverage outputs
3. Low-level requirements are compatible with target computer	MB.6.3.2.c	MB.6.3.2	Confirmation of compatibility between SCADE Suite KCG Metrics and SCADE Suite CVK Limits Analysis of SCADE models complexity with SCADE Suite Metrics and Rules Checker Review of non-automated rules related to model complexity Analysis of SCADE models execution time and memory size with SCADE Suite Timing and Stack Optimizer
4. Low-level requirements are verifiable	MB.6.3.2.d	MB.6.3.2 MB.6.8.1 (see Item 1)	Syntactic and semantic checks automated with SCADE Suite KCG Semantics Checker Analysis of SCADE models complexity with SCADE Suite Metrics and Rules Checker Review of non-automated rules related to model complexity
5. Low-level requirements conform to standards	MB.6.3.2.e	MB.6.3.2	For SCADE built-in rules, syntactic and semantic checks automated with SCADE Suite KCG Semantics Checker For user design rules, peer review or verification automated by SCADE Suite Metrics and Rules Checker
6. Low-level requirements are traceable to high-level requirements	MB.6.3.2.f	MB.6.3.2	Review SCADE-LLRs to HLRs trace data with SCADE LifeCycle ALM Gateway
7. Algorithms are accurate	MB.6.3.2.g	MB.6.3.2 MB.6.8.1 (see Item 1)	Peer review with SCADE LifeCycle Reporter Model simulation of numerical algorithms with SCADE Test
8. Software architecture is compatible with high-level requirements	MB.6.3.3.a	MB.6.3.3 MB.6.8.1 (see Item 1)	Peer review with SCADE LifeCycle Reporter Peer review SCADE HLRs – SCADE architecture allocation matrix
9. Software architecture is consistent	MB.6.3.3.b	MB.6.3.3 MB.6.8.1 (see Item 1)	Syntactic and semantic verification automated with SCADE Suite KCG Semantics Checker Review of SCADE Architecture protection mechanisms against erroneous inputs Review of interfaces with SCADE imported operators
10. Software architecture is compatible with target computer	MB.6.3.3.c	MB.6.3.3	Verification that SCADE Suite CVK tests pass on target Syntactic and semantic verification automated with SCADE Suite KCG Semantics Checker Verification that SCADE Suite KCG Metrics are compatible with SCADE Suite CVK limits Analysis of SCADE models complexity with SCADE Suite Metrics and Rules Checker Review of non-automated rules related to model complexity
11. Software architecture is verifiable	MB.6.3.3.d	MB.6.3.3 MB.6.8.1 (see Item 1)	Syntactic and semantic verification automated with SCADE Suite KCG Semantics Checker Analysis of SCADE models complexity with SCADE Suite Metrics and Rules Checker Review of non-automated rules related to model complexity
12. Software architecture conforms to standards	MB.6.3.3.e	MB.6.3.3	For SCADE built-in rules, syntactic and semantic checks automated with SCADE Suite KCG Semantics Checker For user design rules, peer review or verification automated by SCADE Suite Metrics and Rules Checker
13. Software partitioning integrity is confirmed	MB.6.3.3.f	MB.6.3.3	SCADE Suite introduces no specific risk, but provides no partitioning mechanism; traditional method must be used
MB 14. Simulation cases are correct (see Item 1)	MB.6.8.3.2.a	MB.6.8.1 MB.6.8.3.2	Peer review of SCADE Test verification cases
MB 15. Simulation procedures are correct (see Item 1)	MB.6.8.3.2.b	MB.6.8.1 MB.6.8.3.2	Peer review of SCADE Test verification procedures
MB 16. Simulation results are correct and discrepancies explained (see Item 1)	MB.6.8.3.2.c	MB.6.8.1 MB.6.8.3.2	Analysis of test report generated by SCADE Test Environment

Verification of Outputs and Integration Process‌

Since SCADE Suite KCG Code Generator is a Criteria 1 tool per DO-178C, it is qualified at DO-330 TQL-1. This has the following consequences:

Source code complies with the LLR
Source code complies with software architecture
Source code is verifiable
Source code is traceable to LLR
Source code is accurate and consistent

Related verifications activities are eliminated.

The following table (DO-331 Table MB.A-5) summarizes verification objectives.

Objective Description	Objective Ref	Activity Ref	Verification Method
1. Source code complies with low- level requirements	MB.6.3.4.a	MB.6.3.4	Ensured by SCADE Suite KCG qualification Review of interfaces with SCADE imported operators
2. Source code complies with software architecture	MB.6.3.4.b	MB.6.3.4	Ensured by SCADE Suite KCG qualification
3. Source code is verifiable	MB.6.3.4.c	MB.6.3.4	Ensured by SCADE Suite KCG qualification
4. Source code conforms to standards	MB.6.3.4.d	MB.6.3.4	Ensured by SCADE Suite KCG qualification Verification of compatibility between SCADE Suite KCG metrics and SCADE Suite CVK limits
5. Source code is traceable to low- level requirements	MB.6.3.4.e	MB.6.3.4	Ensured by SCADE Suite KCG qualification
6. Source code is accurate and consistent	MB.6.3.4.f	MB.6.3.4	Ensured by SCADE Suite KCG qualification Additional user integration verification activities to be performed (WCET, Overflow analysis, …)
7. Output of software integration process is complete and correct	6.3.5.a	6.3.5	Analysis of compiling/linking/loading data
8. Parameter Data Item File is correct and complete	6.6.a	6.6	Not SCADE-specific; traditional method has to be used
9. Verification of Parameter Data Item File is achieved	6.6.b	6.6	Not SCADE-specific; traditional method has to be used

Testing of Outputs of Integration Process

The Combined Testing Process (CTP) is a SCADE model-based efficient and optimized testing process to fully satisfy the DO-331 Table MB.A-6 objectives while optimizing testing efforts.

CTP is efficient: test cases and procedures are primarily developed from HLRs. This verification strategy focuses first on HLR functionality and integration issues that are often poorly and lately addressed in a traditional verification process.
CTP optimizes testing efforts: In the context of level A and B applications, the development of test cases and procedures usually requires a huge effort to satisfy all testing objectives. When using SCADE Suite, this testing effort is significantly reduced for the following reasons:
- Regarding the logics (with SCADE Suite), the same requirement-based verification cases and procedures are used for both model simulation on host and testing on target.
- There is no need to develop additional test cases and procedures for logics LLRs that are already covered by HLR-based test cases and procedures. As stated in [DO-178C], §6.4: “If a test case and its corresponding test procedure are developed and executed for hardware/software integration testing or software integration testing, and satisfy the requirements- based coverage and structural coverage, it is not necessary to duplicate the test for low-level testing.”

Factoring simulation and test cases with SCADE Test

The testing effort is mainly focused on HLR-based testing for the application part implemented with Scade.

Factor simulation and test cases with SCADE Test Target Execution

The following table (DO-178C Table A-6) summarizes the verification activities.

Objective Description	Objective Ref	Activity Ref	Verification Method
1. Executable object code complies with high-level requirements	6.4.a	6.4.2 6.4.2.1 6.4.3 6.5 MB.6.8.2.a (see Item 1)	HLR-based normal range testing of SCADE component executable object code in the target environment with SCADE Test Target Execution, user target testing tool, and ALM tool
2. Executable object code is robust with high-level requirements	6.4.b	6.4.2 6.4.2.2 6.4.3 6.5 MB.6.8.2.a (see Item 1)	HLR-based robustness testing of SCADE component executable object code in the target environment with SCADE Test Target Execution, user target testing tool, and ALM tool
3. Executable object code complies with low-level requirements	6.4.c	6.4.2 6.4.2.1 6.4.3 6.5	HLR-based normal range testing of SCADE component executable object code in the target environment with SCADE Test Target Execution, user target testing tool, and ALM tool
4. Executable object code is robust with low-level requirements	6.4.d	6.4.2 6.4.2.2 6.4.3 6.5	HLR-based robustness testing of SCADE component executable object code in the target environment with SCADE Test Target Execution, user target testing tool, and ALM tool
5. Executable object code is compatible with target computer	6.4.e	6.4.1.a 6.4.3.a	HW/SW integration testing of the whole application executable object code

Verification of the Verification Activities

As stated in [DO-178C] §6, the software verification process is a technical assessment not only of the outputs of the software planning process and software development processes but also of the outputs of the software verification process. In this context, we usually talk about the “verification of the verification outputs” with the objective to assess how well the verification activities were performed.

The following table (DO-331 Table MB.A-7) summarizes verification objectives and methods for the verification of verification process results.

Objective Description	Objective Ref	Activity Ref	Verification Method
1. Test procedures are correct	6.4.5.b	6.4.5	Peer review of SCADE Test verification cases and procedures
2. Test results are correct and discrepancies are explained	6.4.5.c	6.4.5	Analysis of test report generated by user target testing environment
3. Test coverage of high-level requirements is achieved	6.4.4.a	6.4.4.1 MB.6.8.2.a	Peer review of HLR-based verification cases and procedures traceability matrices generated by user ALM tool Peer review of SCADE Test verification cases and procedures
4. Test coverage of low-level requirements is achieved	6.4.4.b	6.4.4.1 MB.6.7	Analysis of SCADE Suite model coverage with SCADE Test Model Coverage
5. Test coverage of software structure (modified condition/ decision coverage) is achieved	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 (see Item 1)	Analysis of SCADE Suite model coverage with SCADE Test Model Coverage (observable modified condition/decision coverage), assuming conditions for model to code coverage implication are satisfied
6. Test coverage of software structure (decision coverage) is achieved	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 (see Item 1)	Analysis of SCADE Suite model coverage with SCADE Test Model Coverage (observable decision coverage), assuming conditions for model to code coverage implication are satisfied
7. Test coverage of software structure (statement coverage) is achieved	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 (see Item 1)	Analysis of SCADE Suite model coverage with SCADE Test Model Coverage (influence), assuming conditions for model to code coverage implication are satisfied
8. Test coverage of software structure (data coupling and control coupling) is achieved	6.4.4.d	6.4.4.2.c 6.4.4.2.d 6.4.4.3 MB.6.8.2.b (see Item 1)	Analysis of SCADE Suite model data and control coupling with SCADE Test Model Coverage (influence), assuming conditions for model to code coverage implication are satisfied
9. Verification of additional code, that cannot be traced to Source Code, is achieved	6.4.4.c	6.4.4.2.b	Source code to object code traceability analysis
MB 10. Simulation cases are correct (see Item 2)	MB.6.8.3.2.a	MB.6.8.3.2	N/A
MB 11. Simulation procedures are correct (see Item 2)	MB.6.8.3.2.b	MB.6.8.3.2	N/A
MB 12. Simulation results are correct and discrepancies explained (see Item 2)	MB.6.8.3.2.c	MB.6.8.3.2	N/A

Conclusion

In this blog, we’ve demonstrated how a SCADE model-based approach can fully satisfy DO-178C objectives for the Verification of avionics software.

By optimizing both development and verification processes, the SCADE Suite methodology and tools can deliver up to 50% faster return on investment (ROI) compared to manual coding or alternative non-qualified model-based tools. This is achieved through the use of qualified toolsets and the significant reduction or elimination of debugging, reviews, and verification activities.

DO-178C Level	Level E Cost	Level D Cost	Level C Cost	Level B Cost	Level A Cost
Comparative cost	Baseline	Level E +10%	Level D +36%	Level C +80%	Level B +30%
Cost	100	110	150	270	350+
Cost with SCADE	100	100	120	160	175
Savings with SCADE	–	10%	20%	40%	50%

For more practical information on the accelerated workflow, including a demo video, please refer to this blog article. For a more detailed presentation on achieving DO-178C objectives with SCADE, visit our website.

About the author

Gunther Siegel (LinkedIn) leads the Embedded Software product line within ANSYS. In this role, he acts as the primary technical interface with strategic customers and partners, driving collaboration and innovation Mr. Siegel brings over 15 years of expertise in technical leadership, product development and strategic business growth.