Contents

This post gives a generic description of the S3-based formal safety verification workflows. It starts with a short description of typical safety critical system development processes used in the industry. The two next section gives respectively a brief introduction to the S3 Modeling Languages, and a description of the development of the Safety Specification against which the system is to be verified. The rest of the section presents the S3 workflows together with the architecture and techniques used to ensure the trustworthiness of the solution.

S3 Formal Verification Solution — Introduction (2/4)

Nicolas Breton

2019-12-17 10:44

Contents

Introduction

The ever-rising use of software-based systems to fulfill safety-critical missions calls for methods to ensure the adequacy of these systems to their missions. Most industrial sectors have brought an answer in the form of standards such as EN-50128 for railways, DO-178C for aviation, ISO-26262 for automotive, or more generally IEC-61508 for critical systems. All these standards have in common the central role given to test-based validation techniques. However, alternate and usually complementary techniques, grouped under the banner of “Formal Methods”, are gaining increasing attention for the development and validation of these systems. In particular, the “Model Checking” technique has seen the multiplication of its application fields in the last decade.

S3 Formal Verification — Executive Summary (1/4)

Nicolas Breton

2019-12-16 10:44

Formal Verification is the act of mathematically proving that a system respects some properties under a number of hypotheses. When such a property is proved to hold, it means that it is impossible to find an input scenario satisfying the hypotheses in which the system would falsify this property.

Systerel Smart Solver (S3) is a formal verification solution able to perform a proof of the safety of a critical system after its design (i.e. a posteriori). This solution, combining a specialized modeling language (HLL) with a SAT-based symbolic model checker, has shown to be particularly efficient in handling industrial-size critical systems coming from various domains such as railways or avionics.

A “Chess Game” in Ada 2012?

Robert Cholay

2019-12-09 08:51

Developing a chess game can be a difficult task. This article shows how the implementation of a number of paradigms and services underpinned by Ada 2012 makes it possible to ease this task.

Blog opening

Mathieu Clabaut

2019-12-03 17:10

Systerel opens its blog dedicated to technical topics. You will find there some articles related to Systerel products such as Systerel Smart Solver or S2OPC, but also articles providing feedback on how we work and on the implementation of technologies that we consider interesting in our production environments.

In this way, we imagine that we can provide you with better information on our products and how we work, but also technical guides to address some problems.

Do not hesitate to share back your comments.

Have a good read.