Free Courses

[Solution]

Welcome to the first entry in our series on formal verification, with a special focus on the SCADE Suite Design Verifier. In this blog, we will introduce you to formal methods and the SCADE Suite Design Verifier, setting the stage for deeper dives in future posts.

Upcoming blogs will explore the verification of arithmetic properties, functional and safety properties, and advanced features such as defining sophisticated proof strategies or utilizing multicore processing. Stay tuned!

Introduction

In software engineering, formal methods are rigorous techniques that rely on well-defined mathematical models to specify safety-critical software and prove or disprove its correctness with respect to certain properties. They can also be used in combination with traditional testing methods to automate the generation of test scenarios, which can be particularly tedious when designing complex software systems with hundreds of requirements.

The industrial use of formal methods dates to the past decades with the emergence of the software industry. Since then, formal methods have been applied in many industries including aerospace and railways to meet certification objectives for safety-critical software. In the aerospace industry, the standard RTCA DO-333 — the primary guideline used by certification authorities such as FAA and EASA to approve commercial software-based aerospace systems — provides general guidance that describes how formal methods can be applied within each of the verification activities of safety-critical software to meet the certification objectives.

Recently, formal methods have been introduced in the automotive industry due to the development of autonomous driving vehicles whose design needs to comply with the functional safety standard ISO 26262.

Numerous research works [1] have been led to propose formal languages to specify safety-critical software and to verify their correctness. These languages can be used to build an abstraction of the system model or to formalize the requirements of the system. Among the set of formal languages for developing Safety-critical software, Scade [2] is known to be successful as it has been used for more than two decades to design safety-critical software in many industries including aerospace, nuclear, automotive, and railway. This language is a part of Ansys SCADE Suite, a model-based development environment used for safety-critical embedded software. As a formal language, Scade supports the application of formal methods, enabling rigorous specification, analysis, code generation, and verification of software behavior.

When a software is modeled with formal languages, different formal verification techniques can be used to verify its correctness. In the context of safety-critical software design, model checking, theorem proving, and abstract interpretation are the formal verification techniques used.

As SCADE Suite Design Verifier uses model checking, let’s start by introducing this verification technique before highlighting the tool’s capabilities.

Model Checking

Model checking [3] is a formal verification technique widely used to verify software and hardware systems design. It is a state-based approach that explores all possible states of a formal model in order to determine whether a given property is satisfied by the model.

Model-checking is performed through different steps as described by Figure 1. The first step consists in modeling the system behavior with a formal modeling language and formalizing the system requirements with a property specification language. Then, the system model (M) and the property specification (P) are passed to a model checker which automates the verification process to find out whether the model satisfies the specified properties.

Three scenarios can be observed while running model checking:

• The system model (M) does not satisfy the specified property (P). In this case, a counter example is generated, which can further be used as stimuli in simulation to observe the scenario that violates the property.
• The system model (M) satisfies the specified property (P). In this case, the verification is completed.
• The computation memory is insufficient to complete the verification. In this case, the model checker cannot produce any result.

Figure 1: Description of the model checking workflow (Source: Ansys Inc)

Model checking is the most adopted formal verification approach in the industry when it comes to verifying the functional and safety properties of a software application. Several model checkers have been implemented to verify the functional and non-functional requirements for different kinds of systems. A non-exhaustive list of the most popular model checkers can be found here.

Although model checking is widely used in industry, it is important to mention that this verification technique does not easily scale up since the number of states that could be processed by a checker for system under verification should be small. To overcome this issue, numerous model reduction and abstraction strategies have been developed to deal with state space explosion while running model checking.

SCADE Suite Design Verifier uses some efficient abstraction strategies based on modern SAT-Solvers which reduce significantly the state-space explosion. Future blogs will introduce the verification strategies used in SCADE Suite Design Verifier.

Overview of SCADE Suite Design Verifier

SCADE Suite Design Verifier (SCADE DV) is a model checker tool built on top of Prover PSL®, a well-known proof engine that integrates modern SAT solvers to verify large industrial systems. PSL prover supports bounded model-checking as well as advanced proof strategies such as K-induction and Property Directed Reachability (PDR/IC3), which makes SCADE DV a powerful model-based verification tool. The figure below highlights the capabilities of SCADE DV.

Figure 2: Overview of the SCADE Suite Design verifier capabilities (source: Ansys Inc.)

• Runtime error detection — SCADE DV provides a set of predefined properties (or checks) to check the absence of runtime errors in a Scade model. The runtime errors checked by the tool include arithmetic errors (e.g. division-by-zero, overflows, infinities and NaN) and consistency errors. When a runtime error is detected, a counter example is generated so that designers might fix their errors.
• User-defined property verification — SCADE DV allows users to specify custom properties directly derived from software or safety requirements. These user-defined properties are expressed in the Scade language as Boolean expressions. By using Scade itself as the property specification language, there is no need to introduce or learn a separate formalism —streamlining the verification process and maintaining consistency within the development environment. SCADE DV further checks that the property is always true and generates a counter example otherwise.
• Model coverability analysis — While testing software design, there might be some coverage gaps (i.e. uncovered parts in the software design) due to insufficient test cases, inadequacies in the application requirements or dead and unintended elements in the application design model. These gaps can be filled manually by creating new test cases, updating the existing ones or justifying the uncovered part in the software design. However, depending on the complexity of the software design, manually filling gaps in coverage can be time-consuming. To save time, SCADE DV provides a Coverability Analysis tool that analyzes coverage gaps in a Scade design and automates the generation of test scenarios for the uncovered parts.
• Equivalence verification — When developing software, there might be a need to compare different implementations of the same component to make the right design choice. For this purpose, SCADE DV can be used to check the equivalence of two implementations.

Stay tuned

In this post, we provided a brief introduction to model checking and the capabilities of the SCADE Suite Design Verifier. In upcoming posts, we will dive deeper into the tool’s features and explore its practical applications through examples and use cases.

If you would like to learn more about Ansys SCADE Solutions, we will be happy to hear from you! Get in touch on our product page.

About the author

Dr. Philippe Glanon (LinkedIn) is a technical expert in the design and development of Safety-critical embedded systems and Software. As a senior application engineer at Ansys, he promotes model-based design solutions and he supports customers in aerospace, railways and automotive industries to achieve success through the adoption of SCADE products.

References

[1] “M. Huth and M.D. Ryan: Logic in Computer Science – Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004“, or “K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004“.

[2] “J-L. Colaço, B. Pagano, and M. Pouzet. Scade 6: A Formal Language for Embedded Critical Software Development. In the 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017.

[3] Clarke, Edmund & Emerson, E. & Sifakis, Joseph. (2009). Model Checking: Algorithmic Verification and Debugging. Commun. ACM. 52. 74-84.