Search Results

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.

The ARINC 661 standard [1] defines a Cockpit Display System (CDS) interface intended for all types of aircrafts installations. This paper presents an integrated solution based on Commercial Off-The-Shelf (COTS) tools that allows, in the initial stage of an aircraft project, support for the expression of requirements with regards to the CDS definition and the CDS interaction with the User Applications (UAs). It also enables prototyping of the systems architecture from the point of view of functionalities and performance. At a later stage of the project, this same integrated tool suite can be used to produce and certify the final embedded software code within the CDS and to generate the communication code between the CDS and the UAs.

Development and verification of systems for internal aircraft networks include multiple software layers. These layers are mainly the application-specific components, communication layers, redundancy management and other system services. Verification of these system layers in the early stages of the design process, before a physical network is available, and during the design process has become a critical need in order to reduce design costs and project risks. Time-Triggered Architectures (TTA) and SCADE are both well-established technologies and tools for building safety-critical embedded systems. Both are based on the synchronous paradigm; TTA for the communication infrastructure and distributed embedded computing, and SCADE for simulating and generating code for the application components.

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.

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.