Esterel Technologies>Downloads>White Papers
White Papers
Methodology and Benefits of Timing Verification for Safety-Critical Embedded Software New!
Authored by Thierry LE SERGENT - SCADE Suite™ Product Manager at Esterel Technologies, Reinhold Heckmann - Senior Researcher at AbsInt GmbH, and Daniel Kästner - CTO AbsInt GmbH
Abstract
SCADE Suite™ is a model driven development environment specifically created for system and software developers generating safety-critical embedded systems that require certification according to DO-178B, IEC 61508, EN 50128, or ISO 26262 standards. SCADE Suite's modeling capabilities cover the design, verification, and optimization of complex algorithms, control intensive applications, and control graphic interfaces. Furthermore, SCADE Suite's automatic code generator (KCG) is qualified as a development tool. KCG is delivered with artifacts demonstrating to certification authorities that it was developed in compliance with DO-178B Level A (the highest level of criticality) safety requirements. SCADE Suite KCG™ saves time and money in the costly development and verification activities required by the certification process.
Presented at ERTS 2008
SCADE 6 A Model Based Solution For Safety Critical Software Development
Authored by François-Xavier DORMOY, SCADE R&D Manager at Esterel Technologies
Abstract
SCADE Version 6 is both a language and a Safety Critical Development Environment that brings a new Unified Modeling Style that provides a seamless and safe flow from system to software engineering. This flow relies on strong foundations where safety is considered at each step that allows engineers to focus on key issues whilst removing a significant part of the burden of the development process.
SCADE6 is a model based tool that has been designed to cope with engineers needs together with safety constraints expressed in several standards such as D0178-B, EN50128 or IEC 61508.
This paper presents SCADE version 6 and points out the key factors we have addressed during the language definition, modelling environment and code generation development in order to cope with a safety critical development flow.
Presented at ERTS 2008
A verifiable architecture for multi-task, multi-rate synchronous software
Authored by Jean-Louis CAMUS - Senior Consultant at Esterel Technologies, Pierre VINCENT - Consultant at Esterel Technologies, Olivier GRAFF - Intertechnique, Sébastien POUSSARD - Intertechnique
Abstract
Synchronous model-based software development techniques have proven to be both rigorous and efficient for the development of safety critical real-time software. Currently, the most common practice is to limit the use of synchronous techniques to single tasking or locally synchronous globally asynchronous multitasking scheduling schemes. This paper presents a technique for implementing multi-rate software on several tasks whilst preserving the determinism and verifiability of the synchronous approach. Our technique uses the synchronous framework in order to ensure rigour and verifiability, but implements different parts of a global synchronous model into separate tasks with a simple and efficient architecture. This architecture ensures determinism even in the presence of variations in execution time, and it also allows verification of the complete software by simulation or formal verification. This architecture has been applied to avionics software of a real aircraft's equipment. Further perspectives are also provided.
Presented at ERTS 2008
Combining a High-Level Design Tool for Safety-Critical Systems with a Tool for WCET Analysis on Executables
Authored by Reinhold HECKMANN - Absint, Christian FERDINAND - Absint, Florian MARTIN - Absint, Thierry LE SERGENT - SCADE Product Marketing Manager at Esterel Technologies, Bruno MARTIN - R&D Engineer at Esterel Technologies, Xavier FORNARI - Core Technology R&D Manager at Esterel Technologies, Daniel LOPES - R&D Engineer at Esterel Technologies
Abstract
Synthesizing code from model-based software specifications using automatic code generators such as the SCADE Suite allows design verification at early project stages and helps to avoid coding errors, thus reducing the need for low-level testing. Non-functional properties of the implementation such as execution time and memory consumption require specific analysis. Static program analysis tools like AbsInt's StackAnalyzer and timing analyzer aiT complete ideally the model-based design process with the verification of these properties. These tools can also give SCADE users a direct feedback on the effects of their design decisions on resource usage, allowing them to select more efficient designs and implementation methods. The SCADE tool, StackAnalyzer and aiT can be integrated in a way that the analysis results for code generated by the SCADE tool are conveniently accessible from within the SCADE development environment. We present the tools and their integration, preliminary results, and plans for integration with other tools for timing analysis.
Certified Development Tools Implementation in Objective Caml New!
Authored by Bruno Pagano, Olivier Andrieu, Benjamin Canou, Emmanuel Chailloux, JeanLouis Colaço, Thomas Moniot and Philippe Wang
Abstract
This paper presents our feedback from the study on the use of Objective Caml for safety-critical software development tools implementation. As a result, Objective Caml is now used for the new ScadeTM certified embedded-code generator. The requirements for tools implementation are less strict than those for the embedded code itself. However, they are still quite demanding and linked to imperative languages properties, which are usually used for this kind of development. The use of Objective Caml is outstanding: firstly for its high level features (functional language of higher order, parametric polymorphism, pattern matching), secondly for its low level mechanisms needed by the runtime system (GC, exceptions). In order to develop the tools to check the safety-critical software development rules, it is necessary to reinterpret them for this language, and then to adapt Objective Caml so that it satisfies them. Thus, we propose a language restriction and a simplified runtime library in order that we can define and measure the coverage of a program written in Objective Caml according to the MC/DC criteria. Then we can look forward to seeing this kind of languages spread out the industrial environment, while raising the abstraction level in the conception and implementation of tools for certified programs production.
Certified Development Tools Implementation in Objective Caml. In Practical Aspects of Declarative Languages, 2008. Lecture Notes in Computer Science, vol. 4902, pp. 2-17. http://dx.doi.org/10.1007/978-3-540-77442-6_2 © Springer-Verlag Berlin Heidelberg 2008
Presented at Deutscher Luft- und Raumfahrtkongress 2006
Authored by Jakob Gärtner, Technical Director and Senior Consultant at Esterel Technologies
Abstract
Once upon a time, the world was ideal. Each and every national railway company had its own exclusive chain of suppliers for rolling stock, signalling systems and communication devices. They also had their own standards for signalling and some even owned profiles and track widths. For the exclusively appointed supplier, this meant that he could entirely rely on the business relationship with his (often sole) customer, not fearing any competition whatsoever. A market that is shaped by such static and protectionist approach means that structures, business processes, and development models become exceptionally traditionally and absolutely static and inflexible.
Presented at SpaceOps 2006
Authored by William T. Smithgall
Abstract
Fully integrated space operations demand parallel processing of standardized hardware components that are delivered and integrated just in time to support mission objectives. Flight Software is also a critical component, one that must be customized for each mission, enabling the launch vehicle and payload to perform unique mission objectives. Satisfying these operational needs with a single standardized flight software component, built using current software development practices is notoriously difficult. Modern automated software production tools can now successfully eliminate one or more labor-intensive manual process steps, offering tangible and significant improvement versus traditional software development methods. This paper presents motivations for highly automated production and maintenance of flight software, to satisfy the need for mission customization and product improvement (i.e. new features), while better supporting the just in time delivery and integration goals of modern integrated space operations. Process streamlining, and resulting savings opportunities, will be extrapolated from the current Space Shuttle flight software development process.
Presented at ERTS 2006
Bridging UML and Safety-Critical Software Development Environments
Authored by Alain Le Guennec, Bernard Dion
Abstract
This paper presents an approach combining the respective strengths of UML and SCADE to develop safety-critical systems. By using UML to specify the system's high-level requirements and architecture, and then SCADE to formally specify the software behavior, we provide a seamless flow from the initial requirement analysis phase down to the final integration on the target platform. This flow is based on the connection of UML tools with the SCADE environment, leveraging industry standards such as UML2, XMI, and DO-178B to provide a solution that is exactly tailored to the specific needs of safety critical projects.
Presented at ERTS 2006
Development Approaches in Software Development
Authored by Sylvain Sauvage, Amar Bouali
Abstract
It is a recognised fact that failures in the software design account for an increasing proportion of the car breakdowns. All vehicle functions are concerned, from body and entertainment to chassis and engine management. Even though good practice and better processes have been put at work in many projects, bugs still appear. Easily detectable bugs still pass through and can even have relatively high consequence.
This phenomenon has reached a point where some car manufacturers prefer reducing the number of services offered in the car and putting more effort on controlling the complexity to make software and systems safer.
The introduction of software in the development of safety-related functions will require major process, method and tools improvement. In this paper, we explore the benefits of modelling and accurate software model using tools based on synchronous languages.
Presented at ERTS 2006
Combining Model-Driven Design With Diverse Formal Verification
Authored by P. Amey, Bernard Dion
Abstract
Two historically diverse research streams are now delivering strong industrial performance in the engineering of high-integrity, software-intensive systems. The earlier of these is the use of source-language-based static analysis and formal verification. The more recent is the use of model-driven design coupled with automatic code generation. Although both have been effective, neither is without problems. Fortunately, these approaches are not mutually exclusive and combining them offers a route to ultra-high integrity at low cost. The paper exemplifies the approach by describing the combining of SPARK and SCADE and illustrating the benefits and opportunities that this brings.
Presented at SAE
Formal Verification for Model-Based Development
Authored by Amar Bouali, Bernard Dion
Abstract
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. We conclude by detailing specific formal verification techniques and tools available today for use in a state-of-the-art model-based development environment. We focus on the verification of safety requirements, involving control-logic aspects as well as data computation aspects of embedded software. We explain how to relate this model-checking activity with the objectives of the software life cycle process described in the IEC 61508 standards.
Figures on the use of the SCADE product and its Design Verifier module on several realistic safety-related automotive applications illustrate the presentation.
Presented at JSAE 2005
Using Formal Verification in Real-time Embedded Software Development
Authored by Amar Bouali, Bernard Dion, Kosuke Konishi
Abstract
Model-based development of real-time embedded software using a formal approach provides formal verification as a powerful way to increase the reliability and quality of designs by checking their safety requirements. Formal verification is a cost-effective technique as it saves the effort of writing tests and a checked requirement means the design is correct in 100% of the cases. Additionally, a correct-by-construction automatic code generation ensures that what is verified on the model is verified on the embedded code. Thus, a formally verified specification model can be a strong sign-off between the system requirements and software requirement processes. We illustrate the methodology with the SCADE model-based development environment and a Cruise Control design example. We show the impacts and benefits of using formal verification in software development process.
Presented at Symposium on Formal Methods for Automotive & Transportation
Use of Formal Verification for the Software Development in the Automotive Area
Note: This paper is available courtesy of Volkswagen AG and Audi Electronics Venture GmbH.
The method of Formal Verification is getting more and more important for the software development in the automotive industry because of completeness and the support of Frontloading. This has been investigated for real applications in the context of established tools in this area. Integrating this method into the software development process requires further improvements on the performance, interfaces and supported language of the tools. But in the context of deterministic time triggered architectures, there are additional possibilities to support Frontloading in the development process for software. These interesting topics are represented in this paper.
Presented at SAME Conference 2004 - Winner of "2004 Best Paper" Award
Design and Synthesis with Esterel
Authored by S. Bernardi - Texas Instruments, S. Lebailly - Texas Instruments, B. Blanc - Esterel Technologies, G. Berry - Esterel Technologies, J. Dormoy - Esterel Technologies
Abstract
We describe a practical method for multi-clock design using the formal Esterel language and its programming environment, which is normally limited to single-clock design. The methodology has been applied to two designs at TI. The designs have been fully synthesized and verified.
Presented at Conferences SAE World Congress 2004
Authored by Bernard Dion
Abstract
In this paper, we will describe how synchronous methods form the scientific basis for the creation of a correct-by-construction methodology required for safetycritical 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-byconstruction 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.
Lastly, we will show how a specialized specification to C compiler automated methodology can create embeddable C code that is automatically correct and certifiable to avionics guidelines DO-178B Level A and that makes low-level testing of generated C code unnecessary. Functional testing can be done at graphical specification level and the generated embeddable C code is automatically correct and certifiable.
Authored by Wolfram Hohmann
Abstract
In this paper we will explore how 15 years after being introduced into avionics systems, "by-wire" technologies have entered the automotive world. The use of software within safety-relevant application areas like restraint systems, braking, steering and vehicle dynamics support and control systems, is requiring changes in the processes and methodologies used for embedded software development.
Efficient Development of Airborne Software with SCADE Suite™
Efficient Development of Airborne Software with SCADE Suite™
Authored by Jean-Louis Camus, Bernard Dion
Abstract
This white paper addresses the issue of cost and productivity improvement in the development of safety-critical software for avionics systems. Such developments, driven by the ED-12/DO-178B guidelines traditionally require very difficult and precise development and verification efforts. This paper first reviews traditional development practices and then the optimization of the development process with the SCADE Suite methodology and tool. SCADE Suite supports "correct-by-construction" and automated production of the life cycle elements. The effects on savings in the development and verification activities are presented in detail. Industry examples demonstrate the efficiency of this approach, and business benefits are analyzed.
The Effectiveness of Synchronous Languages for the Development of Safety-Critical Systems
The Effectiveness of Synchronous Languages for the Development of Safety-Critical Systems
Authored by Gérard Berry
Abstract
This paper reviews Synchronous methods and their applicability to the development of critical embedded software, particularly safety-critical embedded software for the avionics industry. The overall idea is to generate correct-by-construction embeddable implementation from high-level rigorous specifications.
Esterel Technologies has commercialized products that implement a correct-by-construction methodology with a sophisticated tool suite. This paper will focus on the application of the SCADE Suite solution. SCADE Suite implements a unified conceptual model of embedded computation backed by three strong technical cores: The use of specific high-level rigorous graphical and textual language; Compiling algorithms for correct-by-construction implementation; and Formal testing and verification techniques.
Simulink™ Users Connect with Esterel's SCADE Suite™ for Safe Embedded Software
Simulink™ Users Connect with Esterel's SCADE Suite™ for Safe Embedded Software
Abstract
Avionics and automotive system design teams use Simulink for fly- and drive-by-wire system modeling and control law validation. SCADE Suite from Esterel Technologies enables embedded software development teams to generate "safe-by-construction" code from formal executable models. By using the SCADE/Simulink Gateway, embedded software development teams can ensure that their code exactly and safely meets the software design requirements, at minimum cost and in a minimum amount of time. This white paper describes the Esterel Technologies Simulink Gateway, and how typical avionics and automotive users are successfully applying SCADE Suite to meet growing safety-critical software development challenges.
From Simulink™ To SCADE/Lustre To TTA: A Layered Approach For Distributed Embedded Applications
From Simulink™ To SCADE/Lustre To TTA: A Layered Approach For Distributed Embedded Applications
Authored by Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis, Peter Niebert, Thierry Le Sergent
Abstract
Designing safety-critical control systems requires a seamless cooperation of tools at several levels - modeling and design tools at the control level, development tools at the software level and implementation tools at the platform level. When systems are distributed, the choice of the platform is even more important and the implementation tools must be chosen accordingly. A tool-box achieving this cooperation would allow important savings in design and development time as well as increases in safety and cost-effectiveness.
In the course of several European IST projects (SafeAir, Next-TTA and Rise), such a goal has been progressively approached and partially prototyped. This paper reports the achievements up to now. The developments were based on the following choice of tools at the different levels: Simulink at the control design level, SCADE/Lustre at the software design level, and TTA at the distributed platform level. Why such a choice?
A Conservative Extension of Synchronous Dataflow with State Machines
Authored by JeanLouis Colaço, Bruno Pagano and Marc Pouzet
Abstract
This paper presents an extension of a synchronous data-flow language such as Lustre with imperative features expressed in terms of powerful state machine `a la SyncChart. This extension is fully conservative in the sense that all the programs from the basic language still make sense in the extended language and their semantics is preserved.
From a syntactical point of view this extension consists in hierarchical state machines that may carry at each hierarchy level a bunch of equations. This proposition is an alternative to the joint use of Simulink and Stateflow but improves it by allowing a fine grain mix of both styles.
The central idea of the paper is to base this extension on the use of clocks, translating imperative constructs into well clocked data-flow programs from the basic language. This clock directed approach is an easy way to define a semantics for the extension, it is light to implement in an existing compiler and experiments show that the generated code compete favorably with ad-hoc techniques. The proposed extension has been implemented in the ReLuC compiler of Scade/Lustre and in the Lucid Synchrone compiler.
The Synchronous Dataflow Programming Language LUSTRE
Authored by N. Halbwachs, P. Caspi, P. Raymond, D.Pilaud
Abstract
This paper describes the language LUSTRE, which is a dataflow synchronous language, designed for programming reactive systems - such as automatic control and monitoring systems - as well as for describing hardware. The dataflow aspect of LUSTRE makes it very close to usual description tools in these domains (block-diagrams, networks of operators, dynamical samples-systems, etc …), and its synchronous interpretation makes it well suited for handling time in programs. Moreover, this synchronous interpretation allows it to be compiled into an efficient sequential program. Finally, the LUSTRE formalism is very similar to temporal logics. This allows the language to be used for both writing programs and expressing program properties, which results in an original program verification methodology.
Synchronous Programming of Reactive Systems
A Tutorial and Commented Bibliography
Authored by Nicolas Halbwachs - Verimag
Formal Verification of an Avionics Sensor Voter Using SCADE
Authored by: Amar Bouali (Esterel Technologies, Samar Dajani-Brown (Honeywell), and Darren Coffer (Honeywell)
Abstract
Redundancy management is widely utilized in mission critical digital flight control systems. This study focuses on the use of SCADE and its formal verification component, the Design Verifier, to assess the design correctness of a sensor voter algorithm used for management of three redundant sensors. The sensor voter algorithm is representative of embedded software used in many aircraft today. The algorithm is captured as a Simulink diagram; it takes input from three sensors and computes an output signal and a hardware flag indicating correctness of the output. This study is part of an overall effort to compare several model checking tools to the same problem. SCADE is used to analyze the voter's correctness in this part of the study. Since synthesis of a correct environment for analysis of the voter's normal and off-normal behavior is a key factor when applying formal verification tools, this paper is focused on 1) the different approaches used for modeling the voter's environment and 2) the strengths and shortcomings of such approaches when applied to the problem under investigation.
High-Level Synthesis From The Synchronous Language Esterel
This paper proposes three techniques aimed to improve the quality of the input to logic synthesis to produce better results.
High-Level Synthesis From The Synchronous Language EsterelAuthored by Stephen Edwards, Department of Computer Science, Columbia University, New York
Type-Based Initialization Analysis Of A Synchronous Data-Flow Language
Authored by Jean Louis Colaço (Esterel Technologies) and Marc Pouzet (Laboratoire LIP6)
Abstract
One of the appreciated features of the synchronous data-flow approach is that a program defines a perfectly deterministic behavior. But the use of the delay primitive leads to undefined values at the first cycle; thus a data-flow program is really deterministic only if it can be shown that such undefined values do not affect the behavior of the system.
This paper presents an initialization analysis that guarantees the deterministic behavior of programs. This property being undecidable in general, the paper proposes a safe approximation of the property, precise enough for most data-flow programs. This analysis is a one-bit analysis - expressions are either initialized or uninitialized - and is defined as an inference type system with sub-typing constraints. This analysis has been implemented in the Lucid Synchrone compiler and in a new Scade-Lustre prototype compiler. It gives very good results in practice.
RSS