Integrating System and Software Engineering for Certifiable Avionics Applications New!

Authored by Frédéric Romeas (Eurocopter) , Thierry Le Sergent, Mathieu Viala, Alain Leguennec (Esterel Technologies)

Abstract

Avionics systems are complex systems that integrate hardware, communication media, have many interactions with other subsystems within or outside of the aircraft, and, for the system discussed in this presentation, integrate software that must be developed according to DO- 178B guidelines. System engineering and software engineering are two engineering disciplines that are historically handled by teams with different cultures, and when their engineering processes are supported by tools, use different, incompatible, tools. This very often leads to difficult collaboration, with at some point redundant information, and inconsistencies.

This presentation introduces a solution, based on standards, SysML for system modeling and on the renowned SCADE Suite® product from Esterel Technologies for the development of DO-178B certified software components.

Formal Model Driven Engineering for Space Onboard Software New!

Authored by Eric Conquet (ESA), François-Xavier Dormoy (Esterel Technologies), Iulia Dragomir (IRIT), Susanne Graf (Verimag), David Lesens (5Astrium Space Transportation), Piotr Nienaltowski (Altran Praxis), Iulian Ober (IRIT)

Abstract

One of the major sources of errors in the development of real time critical embedded software is the misinterpretation of system requirements allocated to the software. These misunderstandings between the system team and the software team may have several sources, but are very often due to the following causes: o Use of ambiguous means to describe the system requirements and the software implementation, leading to different interpretations by the system designers, the software developers and the reviewers. o Insufficient knowledge by the software team of the formalisms and jargons used by the system team, leading to the development of software that does not satisfy the system requirements. o Insufficient knowledge by the system team of the formalisms and jargons used by the software team, leading to inefficient reviews of the software specification and code by the system team. The errors potentially introduced during the development are then generally discovered very late by very costly test processes. From September 2004 to December 2007, the European Space Agency (ESA) led the ASSERT project [1] of the FP6, with the objective of defining a complete system/software engineering process for complex and critical space systems. The ASSERT development process is now supported by a set of tools called TASTE [4]. The main scope of the ASSERT project was the management of non functional requirements, from the capture of system requirements to the automatic generation of code. This paper presents the Full Model Driven Development for On-Board Software project (acronym FMDE), aiming at completing the ASSERT process by the functional approach. It has been co-funded by ESA, Astrium Space Transportation, Esterel Technologies, IRIT (Institut de Recherche en Informatique de Toulouse), Altran Praxis and Verimag.

SCADE System, a comprehensive toolset for smooth transition from Model-Based System Engineering to certified embedded control and display softwareNew!

Authored by Thierry Le Sergent and Alain Leguennec (Esterel Technologies), François Terrier, Yann Tanguy and Sébastien Gérard (CEA)

Abstract

The International Council on Systems Engineering (INCOSE) defines system engineering as an interdisciplinary approach and means to enable the realization of successful systems. It focuses on defining customer needs and required functionality early in the development cycle, documenting requirements, and then proceeding with design synthesis and system validation. The main challenges of system engineering are related to providing non-ambiguous and coherent specification, making all relevant information readily available to all stakeholders, establishing traceability between all activities, and providing the appropriate level of verification and validation. Tools supporting these activities in an efficient way are not yet widely deployed in the industry. Software engineering is done by dedicated teams. Development and verification activities are well supported by model-based tools, particularly when certification objectives, such as DO-178B in the aeronautic industry, are required. It is important that system engineers interact with software development teams to ensure that system requirements are efficiently transferred to the associated software applications. As stated in the SE vision 2020 report specified by INCOSE [1], model-based technology has to play a central role in system engineering. Among the benefits, MBSE shall avoid duplication of information and parallel evolution of data between system teams and software teams, hence reducing the nightmare of information resynchronization.

Policy Paper SCADE KCG and MTC Generic QualificationNew!

Abstract

In the frame of the A400M development, qualification audits have been performed for the tools SCADE KCG and SCADE MTC. On September 7th and 8th, 2010, the versions 6.0.1 and 6.1.2 of the development tool SCADE KCG were audited by DGA-TA and EASA experts. The audit report is referenced as MN1020042_v1.0. EASA and DGA-TA gave their agreement for the qualification of these versions of the tool. On October 20th, 2010, the version 6.1.2 of the verification tool SCADE MTC was audited by DGA-TA expert. The audit report is referenced as MN1023795_v1.0. DGA-TA gave their agreement for the qualification of this version of the tool.

Optimized Safety-Critical Embedded Display Development with OpenGL SC

Authored by Vincent Rossignol - Product Manager - Esterel Technologies

Abstract

Historically, the majority of avionics display manufacturers have sought custom solutions to support the development of cockpit displays, head-up displays and other avionics on-board and ground displays, from specification through to target. This was however a decision borne out necessity rather than choice since the inherent wisdom of a 'commercial-off-the-shelf' (COTS) approach had been understood and demonstrated in other parallel domains for some time. So, with this in mind, why was a more costly custom approach selected?

Developing an Argument for Def Stan 00-56 from Existing Qualification Evidence

Authored by Jean-Louis Camus - Esterel Technologies and Zoe Stephenson - University of York

Abstract

Commonly-used civil guidance and standards in the safety-critical software industry (IEC 61508, EN 50128, DO-178B) constrain development activity and generate process and product evidence. However, procurements for UK defence systems must be supported with a safety case assessed against Def Stan 00-56 Issue 4. This paper studies the use of evidence from civil guidance and standards in arguments towards DS 00-56. The approach is centred on a particular application, the KCG qualified code generator, and is based on a generic software contribution argumentation approach. The results show that issues arise in substantiating failure conditions, choosing a suitable level of detail in the argument and relating detailed explanations to the structure of the evidence. Explicit argumentation was found to be useful in addressing each of these issues.

DO-178C and COTS: Challenges and Opportunities for Avionics Software New!

Authored by Jakob Gartner, Esterel Technologies

Abstract

How the new DO-178C Safety-Standard for Airborne Software will clarify the framework for modern software-development methodologies and the related tools.

Modélisation, vérification et génération de code avec SCADE pour des applications temps réel critiques New!

Authored by Bernard Dion and Amar Bouali, Esterel Technologies

Published in GENIE LOGICIEL Magasine genie-logiciel@orange.fr

Abstract

Cet article présente les techniques de modélisation avancées mises en oeuvre dans l'outil Esterel SCADE® pour le développement d'applications temps réel critiques. La version actuelle, SCADE 6, rassemble dans un même langage une notation à base de schémas fonctionnels, pour décrire la partie calcul, et les machines à états, pour décrire le contrôle. Nous montrons comment la vérification fonctionnelle et non-fonctionnelle de ces applications peut être effectuée sur le modèle de l'application afin de démontrer que celui-ci fournit une réalisation correcte des exigences logicielles de plus haut niveau. Nous présentons enfin la génération de code automatique qui produit un code source efficace, sûr et tra¸able. Ce générateur de code a lui-même été certifié par rapport aux normes internationales en vigueur, telles que la DO-178B pour l'avionique ou l'EN 50128 pour le rail. Des applications industrielles provenant de ces deux domaines sont citées en conclusion pour illustrer le propos.

The Airborne Software Development Challenge

Authored by Jean-Louis Camus, Esterel Technologies

Abstract

Qualified tools can cut software development costs, improve a company's responsiveness and ensure high integrity for airborne software subject to DO-178B. Esterel Technologies' safety manager, Jean-Louis Camus, analyzes how the soon to be finalized DO-178C update may leverage benefits of model-based development with qualified tools.

Understanding How SCADE Suite KCG Generates Safe C Code

Authored by Xavier FORNARI - Esterel Technologies

Abstract

SCADE Suite KCG™ follows a systematic and safe approach to generate C code from a Scade model. This document describes the main characteristics of the C code generated by SCADE Suite KCG 6.1.2 and provides an overview of the data and code structures that are produced.

Relieving Pressure for UAV Software Development

Authored by Jim McElroy, Esterel Technologies

Abstract

The explosive global growth in the requirements and development of Unmanned Air Systems (UAS) and Unmanned Air Vehicles (UAVs) represents both a significant business opportunity and significant risk for those supplier companies willing to engage and address this burgeoning market. There are political and technical challenges ahead that increase both the process complexity of developing such systems and the complexity of the applications themselves. We will focus our energy in this paper on some of the key issues software developers of UAS systems face and how Formal Model-based Development (FMBD) with SCADE can alleviate development pressure under stringent standards such as DO-178B Level A and mitigate risk while making the software developer more productive. FMBD with SCADE has been proven enormously successful on UAVs such as the Neuron (Dassault Aviation), Barracuda (EADS) and the Watchkeeper (U-TacS).

Reaping the benefits of X-by-Wire for Military Land Vehicles

Authored by Ian Hodgson (Esterel Technologies) and Matthias Mäke-Kail (TTTech Computertechnik)

Abstract

X-by-Wire is a generic name given to technologies that seek to replace traditional mechanical control systems with electronic replacements. Pioneered by companies like Airbus in the aerospace domain, the mechanical links that translated the stick or pedal actions of the pilot into movements of the control surfaces were replaced by electrical sensors, computers and servo actuators. The benefits of this transformation of vehicle management apply equally to land- or water-based vehicles as they do to airborne craft. This paper will examine the benefits afforded to the vehicle operators by this technology, as well detailing the experiences of a contributor to an UK MoD funded demonstrator project in the use of two key enabling technologies. The demonstrator project, with goals to investigate safety-critical data buses, development processes, and legislation appropriate to their use on MoD land vehicles, was build upon a small tracked vehicle platform developed as a research platform for a previous program.

Experience Report: Using Objective Caml to develop safety-critical embedded tools in a certification framework

Authored by Bruno Pagano, Olivier Andrieu and Thomas Moniot (Esterel Technologies), Benjamin Canou, Emmanuel Chailloux and Philippe Wang (LIP6), Pascal Manoury (PPS) and Jean-Louis Colaço (Prover Technology)

© ACM, (2009). This is the authors' version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 14th ACM SIGPLAN international Conference on Functional Programming (Edinburgh, Scotland, August 31 - September 02, 2009). ICFP '09. ACM, New York, NY, 215-220. http://doi.acm.org/10.1145/1596550.1596582

Abstract

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE Suite® 6 certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO- 178B, IEC 61508, EN 50128 and such.

Methodology and Benefits of Timing Verification for Safety-Critical Embedded Software

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.

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.

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.

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

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

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.

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.

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.

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.

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.

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.

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.

How to meet EUROCAE ED-12B / RTCA DO-178B international Software safety regulation for airborne systems while reducing development cost

Authored by Bernard DION

Abstract

Aeronautics faces huge challenges imposed by quality, cost and safety in the development of electronic systems. Standardization in system architectures (IMA) and Software development safety guidelines like EUROCAE ED-12B / RTCA DO-178B [1] provide a framework in which should be solved the main problems faced by Software developers in this industry. This paper introduces a methodology that allows the development of safety-critical Software applications in these domains, ensuring that safety guidelines are met while costs are reduced.

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.

Modélisation, vérification et génération de code avec SCADE pour des applications temps réel critiques New!

Authored by Bernard Dion and Amar Bouali, Esterel Technologies

Published in GENIE LOGICIEL Magasine genie-logiciel@orange.fr

Abstract

Cet article présente les techniques de modélisation avancées mises en oeuvre dans l'outil Esterel SCADE® pour le développement d'applications temps réel critiques. La version actuelle, SCADE 6, rassemble dans un même langage une notation à base de schémas fonctionnels, pour décrire la partie calcul, et les machines à états, pour décrire le contrôle. Nous montrons comment la vérification fonctionnelle et non-fonctionnelle de ces applications peut être effectuée sur le modèle de l'application afin de démontrer que celui-ci fournit une réalisation correcte des exigences logicielles de plus haut niveau. Nous présentons enfin la génération de code automatique qui produit un code source efficace, sûr et tra¸able. Ce générateur de code a lui-même été certifié par rapport aux normes internationales en vigueur, telles que la DO-178B pour l'avionique ou l'EN 50128 pour le rail. Des applications industrielles provenant de ces deux domaines sont citées en conclusion pour illustrer le propos.

Open Software Development Platforms for Safety Critical Applications in the Rail/ Transportation Domain

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.

Understanding How SCADE Suite KCG Generates Safe C Code

Authored by Xavier FORNARI - Esterel Technologies

Abstract

SCADE Suite KCG™ follows a systematic and safe approach to generate C code from a Scade model. This document describes the main characteristics of the C code generated by SCADE Suite KCG 6.1.2 and provides an overview of the data and code structures that are produced.

Experience Report: Using Objective Caml to develop safety-critical embedded tools in a certification framework

Authored by Bruno Pagano, Olivier Andrieu and Thomas Moniot (Esterel Technologies), Benjamin Canou, Emmanuel Chailloux and Philippe Wang (LIP6), Pascal Manoury (PPS) and Jean-Louis Colaço (Prover Technology)

© ACM, (2009). This is the authors' version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 14th ACM SIGPLAN international Conference on Functional Programming (Edinburgh, Scotland, August 31 - September 02, 2009). ICFP '09. ACM, New York, NY, 215-220. http://doi.acm.org/10.1145/1596550.1596582

Abstract

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE Suite® 6 certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO- 178B, IEC 61508, EN 50128 and such.

Methodology and Benefits of Timing Verification for Safety-Critical Embedded Software

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.

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.

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.

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

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

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.

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.

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.

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.

The Use of Formal Development Methods for Achieving Medical Device Accountability New!

Authored by Jerry Krasner, Ph.D., MBA

Abstract

A Alternative and Affordable Approach to Enable Medical Device Developers to design better products, save money, meet FDA/CDRH requirements more efficiently, and avoid recalls

Understanding How SCADE Suite KCG Generates Safe C Code

Authored by Xavier FORNARI - Esterel Technologies

Abstract

SCADE Suite KCG™ follows a systematic and safe approach to generate C code from a Scade model. This document describes the main characteristics of the C code generated by SCADE Suite KCG 6.1.2 and provides an overview of the data and code structures that are produced.

Experience Report: Using Objective Caml to develop safety-critical embedded tools in a certification framework

Authored by Bruno Pagano, Olivier Andrieu and Thomas Moniot (Esterel Technologies), Benjamin Canou, Emmanuel Chailloux and Philippe Wang (LIP6), Pascal Manoury (PPS) and Jean-Louis Colaço (Prover Technology)

© ACM, (2009). This is the authors' version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 14th ACM SIGPLAN international Conference on Functional Programming (Edinburgh, Scotland, August 31 - September 02, 2009). ICFP '09. ACM, New York, NY, 215-220. http://doi.acm.org/10.1145/1596550.1596582

Abstract

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE Suite® 6 certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO- 178B, IEC 61508, EN 50128 and such.

Methodology and Benefits of Timing Verification for Safety-Critical Embedded Software

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.

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.

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.

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

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

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.

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.

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.

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.

Modélisation, vérification et génération de code avec SCADE pour des applications temps réel critiques New!

Authored by Bernard Dion and Amar Bouali, Esterel Technologies

Published in GENIE LOGICIEL Magasine genie-logiciel@orange.fr

Abstract

Cet article présente les techniques de modélisation avancées mises en oeuvre dans l'outil Esterel SCADE® pour le développement d'applications temps réel critiques. La version actuelle, SCADE 6, rassemble dans un même langage une notation à base de schémas fonctionnels, pour décrire la partie calcul, et les machines à états, pour décrire le contrôle. Nous montrons comment la vérification fonctionnelle et non-fonctionnelle de ces applications peut être effectuée sur le modèle de l'application afin de démontrer que celui-ci fournit une réalisation correcte des exigences logicielles de plus haut niveau. Nous présentons enfin la génération de code automatique qui produit un code source efficace, sûr et tra¸able. Ce générateur de code a lui-même été certifié par rapport aux normes internationales en vigueur, telles que la DO-178B pour l'avionique ou l'EN 50128 pour le rail. Des applications industrielles provenant de ces deux domaines sont citées en conclusion pour illustrer le propos.

Ein Labor zur modellbasierten Gestaltung interaktiver Assistenz
und Automation im Automotive-Umfeld

Authored by Mark Schröder, Marco Hannibal, Jan Gacnik, Frank Köster, Christian Harms Deutsches Zentrum für Luft- und Raumfahrt (DLR) and Tobias KNOSTMANN - Esterel Technologies

Abstract

Im Rahmen der Entwicklung unmittelbar durch einen Nutzer erfahrbarer Assistenz und Automation ist seine frühzeitige Einbindung in den Gestaltungsprozess durch Präsentation und Evaluation von Prototypen häufig unentbehrlich.

Automotive ECU software development with SCADE Suite New!

Authored by Masaru Kurihara, Electronics Engineering Department, Fuji Heavy Industries

Abstract

In this article the model-based development environment SCADE Suite is introduced to the existing process for development of a motor control unit in an electric vehicle, with particular reference to safe multi-thread executions.

Understanding How SCADE Suite KCG Generates Safe C Code

Authored by Xavier FORNARI - Esterel Technologies

Abstract

SCADE Suite KCG™ follows a systematic and safe approach to generate C code from a Scade model. This document describes the main characteristics of the C code generated by SCADE Suite KCG 6.1.2 and provides an overview of the data and code structures that are produced.

Experience Report: Using Objective Caml to develop safety-critical embedded tools in a certification framework

Authored by Bruno Pagano, Olivier Andrieu and Thomas Moniot (Esterel Technologies), Benjamin Canou, Emmanuel Chailloux and Philippe Wang (LIP6), Pascal Manoury (PPS) and Jean-Louis Colaço (Prover Technology)

© ACM, (2009). This is the authors' version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 14th ACM SIGPLAN international Conference on Functional Programming (Edinburgh, Scotland, August 31 - September 02, 2009). ICFP '09. ACM, New York, NY, 215-220. http://doi.acm.org/10.1145/1596550.1596582

Abstract

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE Suite® 6 certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO- 178B, IEC 61508, EN 50128 and such.

Methodology and Benefits of Timing Verification for Safety-Critical Embedded Software

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.

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.

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.

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

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

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.

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.

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.

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.