Search Results

In this paper, we will describe how synchronous methods form the scientific basis for the creation of a correct-by-construction methodology required for safety-critical embedded systems. We will show how they are applied to software design, validation, and implementation through a process of high-level rigorous specifications, from which we can create correct-by-construction embeddable implementation. The synchronous methods we know today have more than 20 years of scientific research plus ten years of successful industrial application. This paper will explore the basic conceptual model of embedded computation supported by three underlying prerequisites: high-level rigorous graphical and textual languages, compiling algorithms for correct-by-construction implementation, and formal testing and verification techniques.

Formal verification is increasingly used for checking and proving the correctness of digital systems. In this paper, we present formal verification as a cost-effective technique for the verification and validation of model-based safety-critical embedded systems. We start by explaining how formal verification can be easily integrated in a model-based development methodology for critical embedded software. In the methodology examined, the development methods are based upon a formal and deterministic language representation and a correct-by-construction automatic code generation. In this methodology, formal verification proves that what you execute conforms to safety requirements, and what you execute is exactly what you embed. We show the impacts and benefits of using formal verification in software development that must be compliant with the IEC 61508 standards, especially for SIL 3 and SIL 4 software development.

Automotive manufacturers and their suppliers increasingly need to follow the objectives of ISO 26262 as it is now state-of-the art and as it is the case that an ever increasing number of active and passive safety systems are developed within cars. This has increased the need to define a safe system development process. This paper proposes a model-based approach including automatic and certified code generation to efficiently implement the embedded software that controls these systems while meeting the needed safety requirements and obeying the rules of ISO 26262.