Free Courses Fluids Structures Electronics 3D Design Optics Photonics Materials Installation Python Optimization Safety & Cybersecurity Embedded Software MBSE Digital Mission Engineering STEM NVH Student Teams Semiconductors Indo Kursus Partner Courses My Courses

[Solution]

Introduction

In this article, we are going to explain how to save time during Verification & Validation (V&V) activities on software developed with SCADE Suite. V&V is a key activity in the Embedded Software business and can represent 50% of total development costs.

We will explain how to save time during coverage analysis using a feature called “Model Coverage Assistant”. We’ll start by explaining what “coverage analysis” is and the challenges associated with this activity. Then, we will introduce formal methods and discuss how they can help meeting those challenges.

To conclude, we will detail and demonstrate the benefits of this improved V&V workflow.

What is coverage analysis?

Software safety standards in all industries require measuring model coverage and code coverage when running requirement-based test cases.

The objective is to show:

• How thoroughly the SCADE design model has been tested by the software requirements-based tests
• The role of each test case in covering the SCADE model

Depending on the target application safety level, different coverage criteria are mandated. It can either be statement coverage, decision coverage (DC) or modified condition/decision (MC/DC) coverage.

Coverage analysis (or coverage resolution) is the activity consisting in analyzing coverage gaps when exercising requirement-based tests. Addressing uncovered parts through analysis may reveal:

• Shortcomings in the requirements-based test procedures. This requires adding requirements-based test cases.
• Inadequacies in the software requirements. This requires modifying software requirements to increase their precision or remove the inadequacies.
• “Dead” software parts (at model or code level). This requires removing those parts from the model or code.
• “Deactivated” software parts (at model or code level). This requires justifying why the part is deactivated and why it can be left in the application without incurring a safety risk.

What are the challenges associated with coverage analysis?

Coverage analysis can be a complex and time-consuming activity for many reasons:

• This activity is generally performed by the testing team and not the software designers.
• A white-box approach with access to and deep knowledge of the design model is required. This may be contradictory with the independence required for verification activities.
• It may be complex for the team performing the analysis to state that a coverage point is not coverable (in the order of days depending on conditions).
• It is even more complex to arbitrate between a “deactivated” software part that needs an appropriate justification and a “dead” software part that needs removal.
• In many cases, uncovered points that are in fact coverable end up being justified. This may represent a safety issue as the model/code part is not tested.

Formal methods

Formal methods are a group of techniques to check that an application fulfills some selected properties with 100% certainty. They do not necessarily involve scenario execution or simulation. They are based on mathematical reasoning, using the SCADE formalism in the context of the Ansys toolset. SCADE Suite Design Verifier is using formal methods to check properties.

SCADE Suite Design Verifier verification flow

An interesting side effect of formal methods is that when a formal property is falsified, a simulation scenario illustrating a counter-example is generated.

Why is formal verification different from testing?

Traditional testing can reveal the presence of errors but cannot guarantee their absence. Testing can never be exhaustive: bugs may or may not remain in the software.

By contrast, proving a property using formal methods is an exhaustive verification.

Therefore, formal methods are very much complementary to traditional testing.

Benefits of formal methods

SCADE Suite Design Verifier (DV) is built on top of the Prover PSL® SAT-based proof engine by Prover® Technology. It’s a formal verification assistant allowing to save time and effort all along V&V activities. It allows to:

• Identify arithmetic issues, such as divisions by zero, overflows, infinite or NaN values
• Verify equivalence between two design choices/implementations
• Formally express and assess safety properties
• Analyze model coverability & generate testing sequences covering uncovered parts

Benefits of formal methods applied to coverage analysis

Formal methods are used in the SCADE Model Coverage Analysis (MCA) capability. This capability is supported by the SCADE Suite Design Verifier. The principle is rather simple, each uncovered point of the model is translated into a property stating that this point is not coverable/observable and no sequence could lead to its observation. When the Prover engine can proove the property, this means that the coverage point is not coverable. On the other hand, if the property is falsifiable, it means that the coverage point if coverable/observable: a sequence leading to its observation is provided.

It can be used during 2 distinct project phases:

• In the design phase, model coverability analysis can detect and report uncoverable parts of the model. This allows designers to clean up the model and remove uncoverable parts before moving to the testing phase. Designers can also provide relevant justifications for deactivated parts that are non-coverable. These justifications will be part of the design model and will be used during testing.
• In the testing phase, it can analyze uncovered points of the model to either generate a sequence (.sss scenario file) reaching the point or a justification of its uncoverability.

A Model Coverage Assistant (MCA) flow

SCADE Model Coverage Assistant demo

Below is a video demonstrating the Model Coverage Assistant flow on several examples:

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 model coverage assistant feature

Here are the key areas where savings are realized, in safety standards across industries:

Model Based Verification flow with SCADE

As a reminder, here are the objectives automatically fulfilled using a qualifiable code generator:

• Coding Standards
• Trace Source Code to Design Model
• Source Code – Design Model Equivalence Verification
• Conformance to LLR-based Testing (specific to the DO-178C standard)
• Source Code Coverage

Here is the resulting simplified workflow:

Simplified Model Based Verification flow with SCADE

Conclusion

In this article, you saw how Ansys SCADE reduces, automates or removes many V&V activities thanks to the qualification of our code generator (KCG) and testing tools. You also saw how the Model Coverage Assistant capability, powered by SCADE Suite Design Verifier, helps optimize models to improve their testability. Finally, you saw how the Model Coverage Assistant automatically generates test sequences or justifications to increase efficiency during testing.

Customer feedback is that up to 70% savings were observed during the coverage resolution phase, compared to a traditional V&V approach.

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

François-Xavier Dormoy (LinkedIn) is a Senior Product Manager at Ansys. He has been working on the SCADE product for more than 25 years. He specializes in Embedded Software & Systems, Testing, Requirements Analysis, Avionics Design, and DO-178C.