Friday 2 February
Fr.1.A
Software Development
chair : Eric Jenn, Thales Avionics/IRT Saint Exupery - France
Fr.1.A.109:00add Fr.1.A.1 to agenda
Breaking down Silos with contract based design for industrial software development: illustrated through an areospace case study
Contract based approaches have been studied for quite some time but adoption by the mainstream embedded software community and establishing a proper industrial process and methodology has shown to be slow and mainly limited to the architecture team and is not extended to rest of the software teams. This paper presents an integrated development environment for contract based development of embedded systems that addresses a number of challenges in adopting formal methods and contract based approaches. Based on an industrial case study of the development of a controller for trajectory control of a UAV, the paper demonstrates several new features such as architectural system modelling, component interfaces with contract annotations and contract based white box analysis and testing, that move the state-of-the-art in model-driven development with contract based design closer towards managing the industrial complexity of software development and synchronizing the software teams across the entire development lifecycle. The proposed workflow promises a faster development cycle for the different stakeholders of software development: architects, developers and testers. In addition, the methodology promises to provide industrial value in terms of early design error detection, predictable integration of the software, reduced release time and flexible organization level adoption.
Fr.1.A.209:30add Fr.1.A.2 to agenda
Statecharts for Unified Model-Based Design – As simple as possible, as rich as needed
software projects using Simulink or Scade use in fact a subset of Simulink or Scade. The ‘alignment’ of these two subsets gives rise to a new concept, the ‘Unified MBD’, whose data-flow part keeps the expressiveness of both languages and has been introduced in a former paper. Here we present the control-flow part, which is much more restrictive, because the automata paradigms of Scade and Simulink differ fundamentally. But in fact, at least in our context, this loss of expressiveness is not a weakness, because our current design modelling practice is consistent with these restrictions, and because it opens the road for simple but faithful specification modelling practices
Fr.1.A.310:00add Fr.1.A.3 to agenda
Renault Nissan new Software Strategy
The paper presents how, in the context of Embedded Software, Renault and Nissan are addressing the new challenges and define the strategy to face these challenges, such as the increase of functional complexity, or the necessity to deliver much quicker innovations at the right level of quality. We show the major levers that we used in order to improve drastically the robustness of software at launch of new vehicles, such as standardization (AUTOSAR, Genivi, Android), new process, platforming, continuous integration and validation, improvement of quality management system, key principles for a new organization. We then focus on the Alliance Software Center that was completely launched in July 2017.
Fr.1.B
Formal Methods
chair : Laurent Mangane, Airbus - France
Fr.1.B.109:00add Fr.1.B.1 to agenda
CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler
CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This article gives an overview of the use of CompCert to gain certification credits for a highly safety-critical industry application, certified according to IEC 60880. We will briefly introduce the target application, illustrate the process of changing the existing compiler infrastructure to CompCert, and discuss performance characteristics. The main part focuses on the tool qualification strategy, in particular on how to take advantage of the formal correctness proof in the certification process.
Fr.1.B.209:30add Fr.1.B.2 to agenda
Formalise to automate: deployment of a safe and cost-efficient process for avionics software
For over a decade, Airbus have been introducing formal techniques into the verification processes of some of their avionics software products, to cope with the steady increase of the size and complexity of related avionics systems. These techniques have come of age for large-scale industrial deployment. All design and verification processes are currently being revised to take maximum advantage from them, i.e. improve industrial efficiency while maintaining the safety and reliability of avionics systems. To achieve this goal, all human-engineered design artefacts are being formalised using languages with well-defined syntaxes and semantics, in order to allow for the automatic generation of all subsequent, computable design or verification artefacts, and the preparation of the input data for non computable activities. To this aim, several domain-specific languages and related compilers have been developed internally, which cover all design activities, and bridge the gaps to integrate external tools into the overall development processes, e.g. sound, semantics-based, static analysis tools. For instance, the formalisation of detailed designs in the form of function contracts expressed in a first-order logic-based language allows for a hybrid approach to unit verification. Designs may be compiled down to ACSL contracts, allowing for program proof with Frama-C, or they may be compiled down to test contracts, allowing for semi-automatic unit tests.
Fr.1.B.310:00add Fr.1.B.3 to agenda
Proving Properties of Reactive Programs -- From C to Lustre
In critical embedded software, proving functional properties of programs is a major area where formal methods are applied with an increasing success. Anyway, the more a property is complex, the more a high-level formal model of the software and its environment is required. However, in an industrial setting, such a model is not always available, or cannot be used for independent verification. We propose here a new route, where a high-level Lustre model is extracted from a C source program. Hence, high-level functional properties can be specified in Lustre and proved on this extracted model, hence on the real code, without requiring any additional formal documentation.
Fr.1.C
Networks
chair : Marc Boyer, Onera - France
Fr.1.C.109:00add Fr.1.C.1 to agenda
Mixed-Criticality on the AFDX Network: Challenges and Potential Solutions
In this paper, we first assess the most relevant existing solutions enabling mixed-criticality on the AFDX and select the most accurate one. Afterwards, the specification of an extended AFDX, based on the Bust-Limiting Shaper (BLS), is detailed to fulfil the main avionics requirements and challenges. Finally, the preliminary evaluation of such a proposal through simulation is conducted. Results show its efficiency of guaranteeing the highest priority constraints, while limiting its impact on the current AFDX traffic.
Fr.1.C.209:30add Fr.1.C.2 to agenda
Towards Embedded Packet Processing Devices for Rapid Prototyping of Avionic Applications
Recent developments made in the area of network specific reconfigurable hardware and associated description language – namely the P4 language and its back-ends – promise interesting features for rapid prototyping of packet processing devices. Due to the need for high flexibility and increasing trend towards softwarization, such solution is of interest for the aeronautical industry where custom network protocols are generally used. Our contributions in this paper are two fold. First, an analysis of the functionalities of P4 with respect to requirements usually necessary for applications and network protocols in the aeronautic industry is performed. In a second step, a performance evaluation of three different platforms was done. Those platforms represent three use-cases: an existing software-based back-end using Intel DPDK, a hardware network accelerator based on a network processor unit, and an FPGA-based platform. Performance of those platforms are compared to existing state-of-the-art hardware solutions used in by the aeronautical industry.
Fr.1.C.310:00add Fr.1.C.3 to agenda
Next-Gen Train Control / Management (TCMS) Architectures: “Drive-By-Data” System Integration Approach
Based on the European railway industry objectives in the scope of Shift2Rail EU program [1], the work conducted in Safe4Rail (Q4/2016-Q4/2018) [2] proposes a unified embedded platform framework and drive-by-data system integration for the definition of scalable embedded architecture which can integrate critical and non-critical rolling stock / TCMS functions. The proposed architecture enables integration with other railway transportation systems and similar to aerospace IMA, relies on common computing and Ethernet networking resources. The ultimate objective is to create an integrated infrastructure which can host all hard RT, real-time and soft-time functions, and support different models of computation and communication. Such an integrated architecture will reduce lifecycle costs and system complexity of railway TCMS architectures. The key challenges in next generation TCMS are: affordability, complexity, modular certification, frequent dynamic reconfiguration, and the capability to host distributed safety-critical functions. We consider the outcome of this work to be relevant for any future highly integrated and reconfigurable parameter-driven architectures, which requires high levels of software abstraction with support for incremental certification, and rely on new advanced networking approaches related to IEEE TSN, while using the experiences from ARINC 664 and SAE AS6802 standards. The Safe4Rail architecture addresses both safety and security aspects of the embedded platform, and may result in new standards for railway Ethernet networking, including the modifications proposals to IEC61375.
Fr.1.D
Digitalization
chair : Louis-Claude Vrignaud, Continental Automotive - France
Fr.1.D.109:00add Fr.1.D.1 to agenda
Simulation-Based Fault Injection as a Verification Oracle for the Engineering of Time-Triggered Ethernet networks
TTEthernet (TTE) is considered for use as high-speed backbone in the avionics of next-generation orbital space launchers. Given the key role of communication in launchers, the OEM must acquire a precise understanding of TTE’s functioning and its performances in nominal and error conditions. This holds especially true for the clock synchronization algorithm, the cornerstone of time-triggered communication in TTE, which involves complex distributed algorithms. In this study, we use both an experimental platform and fault-injection on a simulation model to gain quantified insights in these questions. We first describe a fine-grained simulation model of TTE model and discuss how it has been validated against communication traces recorded on the TTE platform. We then present experiments that evaluate the accuracy of the clock synchronization in TTE in the fault-free case as well as considering permanent link failure and transient transmission errors. Finally, we discuss what we have learned during the project in terms of development process and programming language support for complex simulation models used in the design of critical systems.
Fr.1.D.209:30add Fr.1.D.2 to agenda
A Deterministic Approach for Embedded Human-Machine Interfaces (HMI) Testing Automation
Human-Machine Interfaces (HMI) have become a central piece of most embedded control systems in many industrial domains. New design techniques have aroused, speeding up the development phases, but the thorough testing of embedded HMIs today remains a largely human-based, time-consuming and error-prone task. While we made in the last decade many improvements in Control software testing, HMI software testing is the area where companies are looking for industrial solution helping them to reduce their cost thus securing their project. This paper presents an innovative embedded HMI testing approach, which aims at reducing the time spent on HMI verification phases, by automating test creation and test results comparison, while ensuring a very high level of determinism and reproducibility.
Fr.1.D.310:00add Fr.1.D.3 to agenda
Co-engineering in aeronautics? The A320 forward section case study
The construction of an aircraft requires the creation of a dedicated industrial system. By industrial system, we mean all the material and immaterial means used to manufacture the object (labour, machines, factories, etc.). Classically, the industrial system is specified after the aircraft architecture was designed. In other words, the specifications of the product are the requirements of the industrial system. The drawbacks of this approach are, firstly, the industrial system can inherit blocking constraints that could be easily removed by changing the aircraft design, and secondly, both continue to evolve during the lifetime of the aircraft. Starting from an industrial case study, the A320 aircraft manufacturing, we proposed, in this paper, to address the problem of having a global view of design and manufacturing for the Aircraft Architect.
Fr. Exhibition visit & Refreshment break (Concorde Room, level -1)
Exhibition visit & Refreshment break (Concorde Room, level -1)
Fr. Keynote Address 4
Keynote Address 4 - Xavier Leroy,
Senior research scientist, INRIA
Fr.2.A
Software Tools
chair : Denis Claraz, Continental Automotive - France
Fr.2.A.111:45add Fr.2.A.1 to agenda
Increase avionics software development productivity using Micropython and Jupyter notebooks
Requirement engineering is a key to understand avionics development productivity. In particular, requirement validation accuracy is considered as the main productivity driver. In this study, we present a typical avionics software development life cycle, and propose a cost model for avionics software development. We provide a method to increase the productivity through early detection of requirement error. Ultimately we present a use case using some cutting edge tools (micropython & jupyter notebook), to achieve requirement validation objective, and increase the overall software life cycle productivity.
Fr.2.A.212:15add Fr.2.A.2 to agenda
Interactive Parallelization of Embedded Real-Time Applications Starting from Open-Source Scilab & Xcos
In this paper, we introduce the workflow of interactive parallelization for optimizing embedded real-time applications for multicore architectures. In our approach, the real-time applications are written in the Scilab high-level mathematical & scientific programming language or with a Scilab Xcos block-diagram ap-proach. By using code generation and code parallelization technol-ogy combined with an interactive GUI, the end user can map appli-cations to the multicore processor iteratively. The approach is eval-uated on two use cases: (1) an image processing application written in Scilab and (2) an avionic system modeled in Xcos. Using the workflow, an end-to-end model-based approach targeting multicore processors is enabled resulting in a significant reduction in devel-opment effort and high application speedup. The workflow de-scribed in this paper is developed and tested within the EU-funded ARGO project focused on WCET-Aware Parallelization of Model-Based Applications for Heterogeneous Parallel Systems.
Fr.2.B
Resilience
chair : Jean-Paul Blanquart, Airbus - France
Fr.2.B.111:45add Fr.2.B.1 to agenda
How Resilient is your computer system?
A system that remains dependable when facing changes (new threats, failures, updates) is called resilient. The fast evolution of systems, including embedded systems, implies modifications of applications and system configuration, in particular at software level. Such changes may have an impact on the dependability of the system. A system is resilient when such changes do not invalidate its dependability mechanisms, said in a different way, current dependability mechanisms remain appropriate despite changes. In this paper we introduce some measures to quantify the capability of a system to remain dependable despite changes, i.e. how resilient it is!
Fr.2.B.212:15add Fr.2.B.2 to agenda
Challenges and Opportunities with Multi-Core Embedded Platform - A Spotlight on Real-Time and Dependability Concepts
Multi- and many-core systems on chip provide an even share of opportunities and challenges regarding the design of modern embedded systems. The FORMUS 3 IC research group is dedicated to investigate these problems and provide novel holistic ideas and solutions for the design process of automotive and avionic applications alike. An extract on new concepts conceived in the context of this project regarding real-time systems and dependability is presented. Furthermore, follow up steps in the development process of these concepts are discussed. In the domain of scheduling, the application of a gang-based scheduling concept for real-time systems is proposed and discussed. This concept aims to allow multithreading in the context of real-time system. Regarding dependability, a fault-tolerance concept based on triple modular redundancy and arithmetic encoding is described. Furthermore, evaluation via fault injection is described and the conceptional work for the fault injection back-end is provided.
Fr.2.C
Field Bus
chair : Thierry Monteil, LAAS - France
Fr.2.C.111:45add Fr.2.C.1 to agenda
Insights on the Performance and Configuration of AVB and TSN in Automotive Ethernet Networks
Switched Ethernet is profoundly reshaping in-car communications. To meet the diverse real-time requirements in automotive communications, Quality-of-Service protocols that go beyond the mere use of priorities are required. In this work, the basic questions that we study on a case-study with diverse and demanding communication requirements is what can we expect from the various protocols aimed at providing a better timing Quality of Service on top of Ethernet? And how to use them? Especially how to use them in a combined manner. We will focus on the Credit-Based Shaper of AVB, the Time-Aware Shaper of TSN and the use of priorities as defined in IEEE802.1Q. The performance metrics considered are the distributions of the communication latencies, obtained by simulation, as well as upper bounds on these quantities obtained by worst-case schedulability analysis. If there have been over the last 5 years numerous studies on the performance of AVB CBS, the literature on comparing AVB to TSN and other candidate protocols is still sparse. To the best of our knowledge, this empirical study is the first to consider most protocols currently considered in the automotive domain, with the aim to gain insights into the different technological, design and configurations alternatives. In particular, an objective of this study is to identify key problems that need to be solved in order to further automate network design and configuration.
Fr.2.C.212:15add Fr.2.C.2 to agenda
Embedded Hybrid Anomaly Detection for Automotive CAN Communication
Due to the steadily increasing connectivity combined with the trend towards autonomous driving, cyber security is essential for future vehicles. The implementation of an intrusion detection system (IDS) can be one building block in a security architecture. Since the electric and electronic (E/E) subsystem of a vehicle is fairly static, the usage of anomaly detection mechanisms within an IDS is promising. This paper introduces a hybrid anomaly detection system for embedded electronic control units (ECU), which combines the advantages of an efficient specification-based system with the advanced detection measures provided by machine learning. The system is presented for - but not limited to - the detection of anomalies in automotive Controller Area Network (CAN) communication. The second part of this paper focuses on the machine learning aspect of the proposed system. The usage of Lightweight On-line Detector of Anomalies is investigated in more detail. After introducing its working principle, the application of this algorithm on the time series of a CAN communication signal is presented. Finally, first evaluation results of a prototypical implementation are discussed.
Fr.2.D
Multicore Implementation
chair : Christophe Moreno, Thales Alenia Space - France
Fr.2.D.111:45add Fr.2.D.1 to agenda
Real-time on-Board Manycore Implementation of a Health Monitoring System: Lessons Learnt
Maintenance has long been a predominant activity in the industrial sector. Measuring and analyzing physical signals on the machines allows to provide a diagnosis on their health state. The more recent Health Monitoring Systems (HMS) allow to optimize the maintenance operations by performing preventive maintenance. The existing HMS are based on various signal-processing algorithms applied to vibration data gathered during flights, in order to compute health indicators. The computation of the indicators is done on-ground, once a full data set has been offloaded. In this paper, we report on experiments made to turn these on-ground computations into on-board real-time computations, using a many-core processor. There are two main issues to be addressed: (i) the management of the flow of inputs from sensors; (ii) the (hopefully tolerable) errors we make when transforming an on-ground algorithm that can treat data globally, into an on-board real-time algorithm that is necessarily incremental. We show that the error is indeed acceptable.
Fr.2.D.212:15add Fr.2.D.2 to agenda
Quality of Service for Integrated Modular Avionics (IMA) on Multicore Processors using a Safety Net Architecture
Tight timing guarantees for COTS multicore processors are still hard or even impossible to provide because of interferences between cores when accessing shared resources like memory or caches. Hence, this kind of processor is rarely used in real-time systems so far. Nevertheless, due to the multicore's clear advantage of saving space, weight, and power compared to multiple single-core legacy systems, many industry domains like avionic have high interest in applying multicores in future products. In this paper an extended version of a non-intrusive online interference detection and quantification approach based on applications' Fingerprints is presented. The Finger printing technology has been extended for application on a real-world avionic Integrated Modular Avionic system. The evaluation shows that the extended approach is able to track the performance of multiple partitions of the system independently. Performance slowdowns above 1.5% are reliably detected and detecting slowdowns higher than 4.8% takes less than 7ms in all cases
12:45 - 13:30
Fr. Lunch (Caravelle Room, level 0)
Lunch (Caravelle Room, level 0) and Closing Session
14:00 - 14:00
Fr. Conference End
Conference end
ORGANISED BY
ERTS 2020 - SAVE THE DATE
January 2020, Wednesday 29 -31
Pierre Baudis Congress Center, Toulouse France
sponsors
-
ADACORE
-
AIRBUS
-
CONTINENTAL
-
GROUPE RENAULT
-
SIEMENS - MENTOR GRAPHICS
-
Institute of Technology Antoine de Saint Exupéry
-
ANSYS
-
QA SYSTEMS
partners
-
AEROSPACE VALLEY
-
ONERA
-
TOULOUSE METROPOLE
-
REGION OCCITANIE / PYRENEES - MEDITERRANEE
media partners
-
L'embarqué
