Introduction

The complexity involved in verifying high-integrity software is fueling a shift towards the use of formal methods and test automation. When validating and verifying high-integrity embedded software, test engineers face several difficult challenges that often account for more than 50% of the cost of a project.

In a Level A (highest safety level) application, DO-178C/DO-331 guidance documents require DC coverage for the model and MC/DC coverage for the code. This activity is effort intensive.

In a previous article, we talked about our new Model Coverage Assistant workflow and how it brings significant savings to safety-critical projects. In this article, we will bring an aerospace color to this message by focusing on projects with DO-178C verification objectives.

Ansys SCADE is widely used for the development of high-criticality DO-178C applications. In this article, we will look at an innovative V&V approach using the SCADE product, enabling you to significantly reduce effort while preserving compliance with DO-178C/DO-331.

This new approach relies on a unique capability: Low Level Test automatic generation.

Details about savings will be provided to show how we can reduce costs, speed certifications and bring products to the market faster. We will conclude by summarizing the actual benefits and describing ongoing work to bring other savings in the future.

History and motivation

In a SCADE Verification Workflow and in accordance with DO-178C Section 6 (objective a., b., and section note), SCADE users do not create Test Cases for Low Level Requirements (LLRs) because LLRs are MC/DC covered by the High Level Requirement (HLR)-based tests. MC/DC code coverage is achieved through HLR-based testing.

DO-178C Section 6

This verification workflow is demanding as it requires manually created, HLR-based tests covering the SCADE Model (the LLRs) for MC/DC criteria. This requires extensive manual effort to create both the HLRs and the HLR-based tests that will trigger the required MC/DC coverage of the SCADE model.

This workflow requires adding some implementation details to HLRs, to reach model (and code) MC/DC coverage. System engineers, that are in general writing that document, are typically not comfortable with this approach.

What enhancement of the SCADE Verification Workflow are we targeting?

Leveraging the formal definition of the Scade language and the power of its formal verification engine (SCADE Design Verifier¹), the new SCADE Verification Workflow aims at automating a significant part of the verification activities by focusing on functionalities and not implementation of the manually created HLRs and by automating the creation of complementary LLR-based tests.

What some customers are expecting is that they want the streamlined SCADE Verification Workflow to be aligned with their organization and move from Example 1 in DO-331 Table MB.1-1 to Example 5:

DO-331 Table MB.1-1

Main benefits are:

• HLRs can focus on functionalities and not implementation details as HLR-based tests must cover the model for Observable DC (ODC) instead of Observable MC/DC (OMC/DC).
• Verification remains a system-level activity (often conducted by system engineers).
• Automating the creation of required (LLR) test cases for MC/DC code coverage leads to significant savings for software engineers.

New verification workflow rationale

In section MB.6.7.1, DO-331 recommends Decision Coverage, and not MC/DC, for model coverage of Level A applications. This is illustrated in Table MB.6-1:

DO-331 Table MB.6-1 Model Coverage Criteria Example

The first three typical completion criteria are included in Decision Coverage defined for Scade Models.

The DC criterion is the required objective at model level to provide evidence of compliance of the model to the HLRs, as specified in DO-331 Sections MB.6.7 and MB.6.8.1 (figure below).

The MC/DC criterion is the required objective at code level to provide evidence of compliance of the code to the HLRs and LLRs (the design model), as specified in DO-178C section 6.4.

DO-331 Table MB.6-8.1 MB.6-7

The table below compares the verification workflow using manual coding, a SCADE workflow before recent improvements, and the new SCADE Model Coverage Assistant workflow.

Manual vs previous vs new workflows

Workflow demo

Below is a video demonstrating the verification workflow:

SCADE V&V workflow benefits

Ansys SCADE offers a greatly simplified model-based verification workflow thanks to:

• A code generator (KCG), qualified at the highest safety levels, that eliminates the need for back-to-back testing and code-level traceability
• A qualified model coverage feature
• The new LLR Test generation capability

Here are the key areas where savings are realized:

Model Based new Verification flow with SCADE

Here is the resulting simplified workflow:

Simplified Model Based Verification flow with SCADE

The table below compares all three V&V workflows: non-SCADE, SCADE (<2022), and the latest SCADE V&V with Model Coverage Assistant. Red denotes the most time-consuming activities, orange marks activities requiring more effort than in other workflows, and green shows optimized processes.

Conclusion

In this article, you saw how Ansys SCADE further reduces, automates or removes many V&V activities thanks to the use of a new LLR Test generation capability.

This alternate verification workflow is already in use on certified operational projects. It satisfies all points of the DO-178C/DO-331 guidance documents. It represents significant savings (30% estimated), already observed by SCADE customers. And it works today!

If you’d like to know more about how Ansys SCADE can improve your testing workflow, you may contact us from the Ansys SCADE Test product page.

About the author

¹ SCADE Suite Design Verifier is powered by Prover PSL from Prover Technology. Prover, Prover Technology, Prover Plug-in, and the Prover logo are trademarks or registered trademarks of Prover Technology AB in European Union, the United States, China, and in other countries.