Free Courses

[Solution]

This article is part of an ECSS blog series. It gives an overview of the European software standards and details the process of developing, then verifying, safe compliant software. You can find links to each part below:

• Part 1: An introduction to ECSS-E-ST-40 Rev.1 and ECSS-Q-ST-80C Rev.2
• Part 2: Efficient Design and Implementation of Safe Space Software in compliance with ECSS-E-ST-40 Rev.1 and ECSS-Q-ST-80C Rev.2 using SCADE Suite
• Part 3 (this blog): Efficient Verification of Safe Space Software in compliance with ECSS-E-ST-40 Rev.1 and ECSS-Q-ST-80C Rev.2 using SCADE Suite

In our previous blog, we have shown how to fully meet ECSS-E-ST-40 Rev.1 and ECSS-Q-ST-80C Rev.2 software design and implementation requirements using the SCADE Suite model-based approach.

In this blog, we provide an overview on how to fully satisfy ECSS-E-ST-40C (Rev.1) and ECSS-Q-ST-80C (Rev.2) verification and validation requirements with a SCADE Suite model-based approach.

Model-Based Development with SCADE

The following figure is a reminder of the software-related processes where SCADE tools are used.

Support of software related processes with SCADE development environment

Software Validation Process

In ECSS-E-ST-40C, software validation refers to software product testing against both the TS (Technical Specification) and the RB (Requirements Baseline). ECSS-E-ST-40C §5.6.3.1a states that “The supplier shall develop and document, for each requirement of the software item in TS (including ICD), a set of tests, test cases (inputs, outputs, test criteria) and test procedures…”.

In Part 2 of this blog series, we have explained that simulation cases and procedures used for model simulation are requirement-based and developed against the TS. SCADE Target Test Execution allows users to translate the requirement-based simulation cases to target test harnesses used for target testing. This is supported by the so-called Combined Testing Process (CTP).

The Combined Testing Process (CTP) is a SCADE model-based efficient and optimized testing process:

• CTP is efficient: test cases and procedures are primarily developed from the Software Requirements Specification, in our case from the TS. This verification strategy focuses first on requirements functionality and integration issues that are often poorly and lately addressed in a traditional verification process.
• CTP optimizes testing efforts: when using SCADE Suite, testing effort of the logics (with SCADE Suite) is significantly reduced: the same requirement-based test cases and procedures are used for both model simulation on host and testing on target.

Factor simulation and test cases with SCADE Test Target Execution

Software Verification Process

Design verification

ECSS-E-ST-40C §5.8.3.3a and §5.8.3.4a require the verification of both the architectural design (including interfaces) and the detailed design.

First, syntactic and semantic checks using SCADE Suite KCG Semantics Checker can be performed to verify that the model follows the rules of the Scade language syntax and semantics (such as type and clock consistency, initialization of data flows, or causality in models).

Second, these verifications can be performed by reviews using the SCADE Architectural Design document and the SCADE Detailed Design document automatically generated by SCADE Suite Lifecycle Reporter. In addition, SCADE Model Change can be used for incremental reviews. The SCADE LifeCycle ALM Gateway supports the allocation of the requirements for the software item to the software components and units. When traceability has been performed, the traceability matrix can be generated from the ALM tool to support the design verification.

SCADE Suite Semantic Checker reporting an error

Code verification

Code verification activities are performed at model level (reviews, testing, etc.). The qualification strategy of SCADE Suite KCG allows SCADE users to generate source code without verifying it (knowing that modification of the SCADE generated code is not allowed).

ECSS-E-ST-40C §5.8.3.5a requires the verification of the software code against 8 objectives. SCADE Suite allows the support of achievement of all of them:

1. The code is externally consistent with the requirements and design of the software item:

The SCADE KCG generated code is consistent with SCADE Suite models: the code implements the SCADE Suite input models only, and the implementation of the models is complete. This is guaranteed by the qualification of SCADE Suite KCG (if a SCADE detailed design model is not correct w.r.t. Scade language definition, no code is generated).

2. There is internal consistency between software units:

SCADE Suite Semantic Checker allows the SCADE user to verify internal consistency between units of a SCADE Suite model.

3. The code is traceable to design and requirements, testable, correct, and in conformity to software requirements and coding standards; and 4. the code that is not traced to the units is justified:

Traceability between a SCADE Suite model and the generated code is ensured by the fact that the code generated by SCADE Suite KCG has been verified as correctly implementing the model’s behavior and by its qualification. The qualification of SCADE Suite KCG has been described in Part II of this series of blogs. In addition, SCADE Suite KCG generates a safe subset of the C language, that is MISRA-C:2024 compliant, and Cert-C:2016 compliant.

5. The code implements proper events sequences, consistent interfaces, correct data and control flow, completeness, appropriate allocation of timing and sizing budgets:

SCADE Suite Semantic Checker allows the SCADE user to verify internal interfaces consistency of a SCADE Suite model as well as correctness of the data and control flow within a SCADE model. SCADE Suite Timing and Stack Optimization computes a safe estimation of the WCET and stack size (i.e., overestimation) for a generic platform. SCADE Suite Timing and Stack Verifier Gateway for AbsInt aiT (TSV) is a gateway to the AbsInt aiT tool enabling to compute precise WCET and stack size for a model on a specific hardware target. These facilitate estimation and allocation of time and size budgets of a SCADE Suite application.

6. The code implements safety, security, and other critical requirements correctly as shown by appropriate methods; and 8. the effects of any residual runtime errors are controlled through error handling:

Verification of implementation of safety, security, and other critical requirements as well as the implementation of residual runtime errors handling mechanisms can be performed by reviews, supported by the SCADE Detailed Design document generated by SCADE Suite Lifecycle Reporter. SCADE Model Change can be used for incremental reviews.

7. The code is implemented in a way that it cannot result in runtime errors:

SCADE Suite Design Verifier (which is a formal verification tool) is able to prove properties of the SCADE model and can be used to prove the absence of:

• Integer division by zero
• Integer overflow
• Float infinity
• Float Not-a-Number

In addition to these objectives, ECSS-E-ST-40C Annex U provides 14 checks that are expected to be performed on the software code. SCADE Suite supports the achievement of all of them as follows:

1. The code implements numerical protection mechanisms (e.g., against overflow and underflow, division by zero): SCADE Suite Design Verifier allows users to identify: in a SCADE Suite model:

• Integer division by zero
• Integer overflow
• Float infinity
• Float Not-a-Number.

2. The code does not perform out of bounds accesses – e.g., underrun or overrun of buffers, arrays or strings: the Scade language does not allow users to incorrectly access memory through pointers or to express an array access that could be out of bounds. This is preserved within the automatically generated code.

3. The code does not include any infinite loop other than the main loop of the software and the main loops of cyclic tasks: the Scade language allows only bounded loops, using constant values known at code generation time. Consequently, the generated code contains neither infinite loops nor recursive functions.

4. The code appropriately uses arithmetic and logical operators (e.g., arithmetic OR vs. logical OR): the Scade language is strongly typed. Arithmetic operators use numeric types while Boolean operators use bool type. This is preserved within the automatically generated code.

5. Implicit type conversions do not lead to arithmetic errors: there are no implicit type conversions in the Scade language. This is preserved within the automatically generated code.

6. The lifetime of variables is consistent with their use: a variable generated by the qualified SCADE Suite KCG code generator remains valid and accessible in memory for exactly how long it needs to be used.

7. The code makes proper use of static/global functions/variables to enforce the correct level of visibility: the Scade language does not allow user-defined global variables.

8. The code makes proper use of volatile variables for all variables that can be modified asynchronously (e.g., hardware access, memory-mapped I/O): this is not allowed as Scade is a synchronous data flow language.

9. The code does not perform invalid memory accesses (e.g., dereferencing null pointers): memory allocation is fully static within Scade language. There is no possibility to incorrectly access memory through pointers or an index out of bounds in an array. This is preserved within the automatically generated code.

10. The code does not access uninitialized variables: a SCADE model is guaranteed to not depend on an uninitialized variable. This is preserved within the automatically generated code.

11. The code does not perform unused assignments, unless this is done to trigger HW side-effects: SCADE Suite Semantic Checker detects unused variables.

12. There are no memory leaks: In the Scade language, memory allocation is fully static (no dynamic memory allocation). This is preserved within the automatically generated code.

13. Pointer arithmetic is justified and operand types are consistent: in the Scade language no dynamic address calculation is performed (no pointer arithmetic). The Scade language is a strongly typed language, with no implicit type conversions. This is preserved within the automatically generated code.

14. The code does not lead to race conditions: a correct SCADE model is guaranteed to be deterministic (given an input sequence, a unique output sequence is produced). Consequently, there are no race conditions. This is preserved within the automatically generated code.

Code coverage measurement

Code coverage measurement is required by ECSS-E-ST-40C §5.8.3.5b. The figure below provides the coverage goals per software criticality category. Some of these must be agreed between the customer and the supplier (ECSS-Q-ST-80C §6.3.5.2).

ECSS-E-ST-40C §5.8.3.5b notes as well that achieving code coverage goals shall be met by running unit, integration and validation tests, measuring the code coverage, and achieving the code coverage by additional (requirement based) tests, inspection or analysis.

ECSS-E-ST-40C §5.8.3.5b

Code coverage goals

Within the SCADE Suite environment, coverage is measured at model level. Model coverage analysis assesses how thoroughly the SCADE model is exercised during model simulation using the requirement-based test 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 test 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.

Specific model coverage criteria for SCADE Test Model Coverage have been designed to:

• fit the entire Scade language: data flow constructs as well as logic-oriented constructs (state machines, clocked blocks)
• provide a sound and accurate assessment of the fact that every model construct and flow are exercised during model simulation

SCADE Test Model Coverage criteria are as follows: Influence, Observable Decision Coverage (ODC) and Observable Modified Decision Coverage (OMC/DC). Following Table shows the correspondence between the coverage criteria of SCADE Test Model Coverage (Influence, ODC, OMC/DC) and the code coverage criteria of ECSS-E-ST-40C.

Model-level Coverage Criterion	Code-level Coverage Criterion
Influence	Statement Coverage
ODC	Decision Coverage
OMC/DC	MC/DC

SCADE Test Model Coverage guarantees that coverage at model level implies code coverage at the proper level (statement coverage, decision coverage, and MC/DC), when SCADE Suite KCG is used to generate the source code. To preserve the coverage implication, SCADE Test Model Coverage shall be used in compliance with the usage conditions stated in the SCADE Test Model Coverage certification kit.

More details about SCADE Test Model Coverage are available here.

SCADE Model Coverage

In order to support the achievement of model coverage, SCADE Design Verifier enables users to perform coverability analysis to detect the uncoverable parts of the SCADE model during the software design phase, which allows an early consideration of the objective. In addition, SCADE Test Environment for Host (TEH) provides a coverage assistance tool which enables users to analyze uncovered parts of the design and generate either a sequence reaching this part or a justification of its non-coverability.

SCADE Design Verifier Coverability Analysis

Verification of source code robustness

ECSS-E-ST-40C §5.8.3.5f requires the usage of static analysis to verify the robustness of the source code and identify the errors that are difficult to detect at runtime.

SCADE Suite KCG Semantic Checker verifies SCADE Detailed Design models against all syntax and semantic rules of the Scade Language Reference Manual. This includes but is not limited to:

• detection of missing definitions
• warnings on unused definitions
• detection of dependency to an uninitialized flow
• type consistency check of operator instance actual parameters with operator interface
• detection of causality issues, i.e., immediate dependency of a flow definition with on the flow itself
• clock consistency checks to ensure that flows are produced and consumed at the same rate.

Robustness of safety critical software cannot be addressed locally. It requires a general robustness policy for the whole system and should be addressed at each step of the development and verification processes. The robustness policy should be defined in the Software Design Standards, Software Coding Standards, and Software Architecture Design Document. As an example, the way of handling arithmetic exceptions should be defined at this global level. There should be explicit decisions about robustness and failure handling in the software requirements which should specify responses to abnormal input data and to any invalid data that may be produced by computation described in the SRS. This is required to achieve accuracy and determinism of requirements and to perform requirements-based testing for robustness tests.

Verification of software unit testing

SCADE ALM Gateway enables traceability from software requirements to SCADE Test procedures allowing the verification of consistency between the unit tests and SCADE Detailed Design model and software requirements. The qualification of SCADE TEH ensures that simulation results are correctly evaluated. These simulation results are reviewed to confirm that they are compliant with expected results (ECSS-E-ST-40C §5.8.3.6a).

Schedulability analysis and feasibility of the design

In SCADE Suite, concurrency is expressed functionally in the SCADE Suite models. SCADE Suite KCG considers the model structure to generate sequential code, considering this functional concurrency and the data flow dependencies.

Schedulability is guaranteed (provided that there is no error raised by SCADE Suite KCG Semantic Checker).

Technical budget management

Timing and Stack Optimizer Analysis Graph

ECSS-E-ST-40C §5.8.3.12 requires the estimation of the technical budgets (including memory size, Processing Unit utilization, etc.) as part of the verification of the software requirements, software architectural design and software detailed design. The technical budgets shall be updated with the measured values and shall be compared to the margins as part of the verification of the coding, testing and validation. SCADE Suite Timing and Stack Optimizer (TSO) allows users to compute a safe estimation (i.e., overestimation) of the WCET and stack size for a generic platform.

To optimize the estimations, SCADE Suite Timing and Stack Optimizer can be used to iteratively:

• focus on the application parts causing long execution times or unsatisfactory memory usage and refine the application profiling by optimizing SCADE Suite models, and/or
• tune SCADE Suite KCG code generator options.

SCADE Suite Timing and Stack Optimizer allows users to generate a diff report showcasing the impacts of above optimizations on WCET and stack size estimation.

TSO Session Comparison

SCADE Suite Timing and Stack Verifier Gateway for AbsInt aiT is a gateway to the AbsInt aiT tool enabling its users to verify timing and stack usage requirements for the SCADE Suite generated code on a specified target processor. It estimates Worst-Case Execution Time (WCET) and the maximum stack size required by the application and reports the results at model level within SCADE Suite. The measurements can be compared to the estimates to determine whether they remain within the defined margins. The cross-compiler options can be tuned to support the optimization of measured values.

Verification of behavior modeling

Verifying the software behavior using the software behavioral design model (Ref ECSS-E-ST-40C §5.8.3.13) is performed by simulating the SCADE Suite model, as this model includes the behavioral view. The SCADE model simulation consists in executing the model to verify its behavior against expected outcomes.

In addition, SCADE Suite development environment provides a powerful visual debugging environment that enables definition of stop conditions, setting breakpoints within a clock cycle, and examination of the internal variables and output values. It is also possible to record and play back scenarios. The behavior of the SCADE Suite model can be verified using these capabilities. It is also possible to record and play back scenarios. The ASCII format of the scenarios makes it easy to integrate within existing workflows. Debugging tasks can be tailored and automated using Python or TCL (Tool Command Language) scripting languages.

The SCADE Suite design can also be reused by directly integrating the generated code or a FMU in a system level simulator.

SCADE Suite Simulation

Software Security process

ECSS-E-ST-40C and ECSS-Q-ST-80C standards have been updated to integrate a software security process that is performed during the full lifecycle of the software. “It is supported by a software security analysis that is systematically maintained at different points in the lifecycle of the software.” (ECSS-E-ST-40C §4.2.11). Ansys medini analyze Cybersecurity Pro can be used to perform security and vulnerability analyses.

ECSS-Q-ST-80C (Space product assurance – Software product assurance)

ECSS-Q-ST-80C brings additional considerations related to tools selection and automatic code generation:

Requirements about tools and supporting environment

ECSS-Q-ST-80C §5.6.2.2a requires to justify the suitability of the software development environment.

SCADE Suite is the best fitted development environment. As SCADE stands for “Safety-Critical Application Development Environment”, it has been developed specifically for the development of safety critical software.

The cornerstone of SCADE is the Scade language which relies on the theory of synchronous languages for real-time applications. SCADE Tools are extensively used in aviation, nuclear, railway industries, and have been audited successfully by various aviation, nuclear and railway certification authorities.

Requirements in case of automatic code generation

Tool selection

When selecting a tool for automatic code generation, ECSS-Q-ST-80C §6.2.8.1a requires the supplier to evaluate following aspects:

• evolution of the tools in relation to the tools that use the generated code as an input: SCADE Suite KCG generated code is compliant to [C-ISO] making it portable and facilitating the interface with other tools.
• customization of the tools to comply with project standards: SCADE Suite KCG can be customized using code generation options to comply with project standards.
• portability requirements for the generated code: SCADE Suite KCG generates code that is operating system independent and compliant to [C-ISO]
• collection of the required design and code metrics: SCADE Suite KCG computes complexity metrics for the KCG generated C code. In addition, SCADE Suite Rule Checker allows SCADE users to automatically check complexity rules w.r.t. the model complexity metrics defined in the SCADE Suite Software Modeling Standard (for example: Number of hierarchical levels of conditional blocks, Number of diagrams defining an operator, etc.).
• verification of software components containing generated code: verification activities are performed at model level. SCADE TEH provides an integrated environment that allows the verification of the SCADE Suite models.
• configuration control of the tools including the parameters for customization.
• compliance with open standards: SCADE Suite KCG is qualified as per requirements of (see 4.2):
  • DO-178C/DO-330 TQL-1 for usage up to DAL A
  • ISO 26262 TCL 3 for usage up to ASIL D
  • IEC 61508 T3 for usage up to SIL 4
  • EN 50716 T3 for usage up to SIL3/4

SCADE Suite KCG development has been audited by TÜV which issued certificate of compliance with ISO 26262, IEC 61508 and EN 50716 standards.

Tool qualification

In case of automatic code generation, ECSS-Q-ST-80C §6.2.8.3a states that “The required level of verification and validation of the automatic generation tool shall be at least the same as the one required for the generated code, if the tool is used to skip verification or testing activities on the target code.” Since in the case of SCADE development environment, the verification activities are performed at model level, SCADE Suite KCG has been developed as per requirements of above-mentioned safety standards. This qualification strategy is even more stringent than what is requested by §6.2.8.3a as SCADE Suite KCG has been developed in accordance with a safety standard (IEC 61508-3:2010).

Requirements related to coding

ECSS-Q-ST-80C §6.2.8.6a states that “§6.3.4 shall apply to automatically generated code, unless the supplier demonstrates that the automatically generated code does not need to be manually modified”. When using the SCADE Suite development environment, verification activities are performed at model level. The qualification strategy of SCADE Suite KCG allows its users to generate source code without verifying it. Thus, clause 6.3.4 of ECSS-Q-ST-80C doesn’t apply in our case.

Conclusion

In this blog series, we have shown how a SCADE model-based approach can satisfy software engineering objectives of ECSS-E-ST-40C and ECSS-Q-ST-80C standards.

SCADE Suite methodology and tools accelerate ROI by up to 50% through optimized development and verification workflow compared to manual coding or alternative non-qualified model-based tools. Usage of SCADE qualified toolsets minimize or eliminate debugging, reviews, and verification tasks, boosting process efficiency.

For more practical information on the accelerated workflow, including a demo video, please refer to this blog article.

If you would like to learn more about Ansys SCADE, we’d love to hear from you! Try SCADE with a free SCADE Student license, or get in touch on our product page.

About the author

Amina MEKKI-MOKHTAR (LinkedIn) is a Safety Manager and Senior Software Safety Expert for Synopsys. She is an active member of several safety standardization committees working on IEC 61508-3, ISO 26262, ISO PAS 8800, ISO/IEC TS 22440, DO-178C and its supplements, etc. She has experience in software safety, software architecture, certification, model-based development, safety analyses, safety audits, and tool qualification. She has an engineering degree in computer science, master’s degree in cyber security and PhD in dependable computing.