Download Th.Keynote Address 3 presentation

Th.Po.109:45add Th.Po.1 to agenda

Download Th.Po.1
Download Th.Po.1 presentation

Profiling Two Broadcast Protocols for Transiently Powered Wireless Sensor Networks

David Richardson - Department of Computer Science, The University of Warwick, United Kingdom Arshad Jhumka - Department of Computer Science, The University of Warwick, United Kingdom

Transiently powered wireless sensor networks (TPWSNs) introduce computing problems that are not faced by traditional wireless sensor networks. Motes in a TPWSN may crash and later recover at an arbitrary time due to their power cell being drained and subsequently recharging to a point where the mote can resume its task. During the crash, a mote loses its state which may have to be later reacquired upon restart. To reduce the overhead of recomputing a current state, techniques such as checkpointing have been proposed. However, we conjecture that there are protocols that are tolerant to such intermittent crashes. As such, in this paper, we compare two broadcast protocols in the presence of transient power faults. We investigate their efficiencies through the message coverage metric, a measure of how many motes receive a message. Coverage for both protocols is measured with different mote failure schemes, recovery times, and maximum simultaneous failures. We find that the Trickle protocol performs the best across all experiments, reaching almost 100% message coverage in certain situations.

Th.Po.209:45add Th.Po.2 to agenda

Download Th.Po.2
Download Th.Po.2 presentation

Anomaly detection using hardware performance counters on a large scale deployment

Malcolm Bourdon - EDF R&D, LAAS-CNRS, France Eric Alata - LAAS-CNRS, France Mohamed Kaaniche - LAAS-CNRS, France Vincent Migliore - LAAS-CNRS, France Vincent Nicomette - LAAS-CNRS, France Youssef Laarouchi - EDF R&D, France

The last recent years witnessed a massive and fast_x000D_ deployment of Internet of Things (IoT) devices. Most of them_x000D_ have not been designed with a careful analysis of security_x000D_ requirements, which makes them likely to include multiple_x000D_ vulnerabilities. Moreover, as these devices include various_x000D_ communication interfaces, they have become a privileged target_x000D_ for attackers. As a consequence, large scale attacks, such as_x000D_ Mirai, must be considered seriously and it is crucial to design_x000D_ and implement protection and intrusion detection mechanisms_x000D_ to mitigate the threats associated to the use of IoT devices in_x000D_ our daily activities as well in critical environments._x000D_ This paper proposes an anomaly detection approach, in_x000D_ the particular context of a large scale deployment of identical_x000D_ IoT devices. Furthermore, we consider an attacker who can_x000D_ install and execute malicious software while continuing to_x000D_ execute legitimate software, in order to stay invisible as much_x000D_ as possible. The approach is based on the statistical analysis_x000D_ of Hardware Performance Counters (HPC) collected at a_x000D_ regular basis from these identical devices, and to highlight the_x000D_ outliers corresponding to significant deviations with respect_x000D_ to normal usage scenarios. This idea relies on the intuition_x000D_ that it is very difficult for the attacker to add some malicious_x000D_ software in a corrupted device without perturbing the HPCs._x000D_ This paper presents this approach and the first experiments_x000D_ carried out to assess its relevance.

Th.Po.309:45add Th.Po.3 to agenda

Download Th.Po.3
Download Th.Po.3 presentation

Interaction-oriented programming for Cockpits and Controller Working Positions

Stéphane Conversy - ENAC, France

Despite their pervasiveness, interactive software are still notoriously difficult to conceive and maintain. In previous work, we proposed a software execution model, a software architecture (djnn) and a language (smala), whose combination provides the basis of what we call interaction-oriented programming. We have demonstrated its use in 2 cockpit HMIs. Here we show our work-in-progress at programming a highly interactive flight preparation HMI, and a radar for cockpit and for a controller working position able to interactively display thousands of elements. This work suggests that interaction-oriented programming with djnn and smala might be suitable for a class of aeronautical onboard and ground applications.

Th.Po.409:45add Th.Po.4 to agenda

Download Th.Po.4
Download Th.Po.4 presentation

Toward real-time embedded observer of unsteady fluid flow environment

Valentin Resseguier - Lab, SCALIAN DS, France Matheus Ladvig - Lab, SCALIAN DS, France Agustin Martin Picard - Lab, SCALIAN DS, France Etienne Memin - Fluminance team, Inria, France Bertrand Chapron - LOPS, Ifremer, France

For monitoring and actively controlling hydrodynamic and aerodynamic systems (e.g. aircraft wing), it can be necessary to estimate in real-time and predict the flow around those systems. We propose here a new method which combines data, physical models and measurements in this purpose. Very good numerical results have been obtained on 2- and 3-dimensional wake flows at moderate Reynolds, even 16 vortices shedding cycles after the learning window.

Th.Po.509:45add Th.Po.5 to agenda

Download Th.Po.5
Download Th.Po.5 presentation

A user privacy-centric access control policy of data for intelligent transportation systems

Rémi Adelin - LAAS-CNRS, France Eric Alata - LAAS-CNRS, France Vincent Migliore - LAAS-CNRS, France Vincent Nicomette - LAAS-CNRS, France

Intelligent Transportation Systems have a variety of application, from improving transportation safety and traffic management to infotainment. The development of these systems includes the deployment in the vehicle of sensors that collect data and share them with actors having different profiles, roles and motivations. These data may concern the private life of drivers, who, most of the time, are not aware of the recipients and of the usage of their data. A key issue is to give to drivers control of their data. For that purpose, we propose in this paper a flexible and fine-grained access control policy of data, based on Attribute-Based Encryption, designed to protect drivers privacy. We also provide a description of the security architecture to enforce such an access control.

Th.Po.609:45add Th.Po.6 to agenda

Download Th.Po.6
Download Th.Po.6 presentation

EMBEDDED FRANCE new Organization and Missions

Cendrine Barruyer - Embedded France, France Cedric Demeure - Thales, France Olivier Guetta - Renault, France Jean-Luc Chabaudie - Altran, France

Embedded France is the association of French players in embedded software and systems. This non-profit organization acts as the armed wing of the French State (DGE) within the embedded ecosystem to promote “skills sharing” and cross fertilization, and brings together all stakeholders in the sector: researchers, training centers, industrialists. It was created in 2013 with the main objectives of developing activities in the domain and contributing to the competitiveness of the French Industry. Embedded France is a unique association because of its transversality. It brings together players of all sizes, from major contractors and competitiveness clusters, to emerging startups, as well as universities and engineer schools. This paper will first recall the main missions of this association, then, it will describe the new governance recently reshuffled to improve its attractiveness and the associated roadmap, and will at the end focus on the various ongoing Working Groups.

Th.Po.709:45add Th.Po.7 to agenda

Download Th.Po.7
Download Th.Po.7 presentation

Efficient refactoring in industrial projects

Flavien Huynh - Vector, France Cyril Benkimoun - Vector, France

Software projects are expanding on several fronts: source code size growth, multiple developing teams, diversity of coding languages and standards. Maintaining control over these projects requires limiting of code size explosion, tight monitoring of Technical Debt, and clear understanding of what should be monitored (new code) or not (legacy code). In these conditions, code refactoring can become a lengthy and hazardous task. We propose a solution pointing to the best candidates for code refactoring. This method uses results of algorithmic cloning detection, Technical Debt computation, and code stability monitoring. Used in a Continuous Integration chain, this solution can not only help optimize refactoring effort, but also focus on relevant areas first, all the while monitoring ongoing developments.

Th.Po.809:45add Th.Po.8 to agenda

Download Th.Po.8
Download Th.Po.8 presentation

Validating the Numerical Accuracy of Critical Systems: A Case Study with Spoat and Space Launcher Flight Software

Corentin De Souza - Numalis, France Ludovic Gauthier - Numalis, France Arnault Ioualalen - Numalis, France David Lesens - Ariane Group, France Matthieu Martel - Université de Perpignan Via Domitia, France Philippe Miramont - CNES, France

It is well-known that numerical computations are sensible to the computer arithmetic which introduces roundoff errors and possibly makes the results of programs inacurrate. This risk has to be considered in the verification and validation (V&V) phases of a critical system and the needs for V&V techniques increase as quickly as critical tasks relying on complex computations are delegated to computers, for example in cars, aircrafts or space vehicles._x000D_ _x000D_ Numalis is a company specialized in the reliability and optimization of numerical accuracy. Numalis software suite aims at bringing solutions for V&V and for the optimization of numerical codes. In particular, Spoat is a V&V tool for numerical accuracy developed by Numalis which performs static and dynamic analyses of source codes in order to determine the worst losses of numerical accuracy on the output_x000D_ variables of programs. Spoat's static analyzer has been used by ArianeGroup in order to evaluate how the tool could be used at the V&V level for critical software such as space launcher flight software.

Th.Po.909:45add Th.Po.9 to agenda

Download Th.Po.9
Download Th.Po.9 presentation

Dynamic virtual platform for HW/SW partitioning on MPSoC platforms

Adrien Thierry - Space Codesign Systems, Canada Hubert Guerard - Space Codesign Systems, Canada Guy Bois - Polytechnique Montreal/Space Codesign Systems, Canada

Nowadays, programming complex integrated Multi Processor Systems-on-Chip (MPSoCs) requires a design flow that offers joint support for both hardware and software. Such a flow must be simple enough to warrant its use. The flow must also provide insightful feedback about the optimization choices available to achieve the required performance goals. This paper focuses on virtual platforms, more specifically on the hardware/software codesign methodology. We present a new type of virtual platform named dynamic virtual platform and we show its benefits compared to the traditional virtual platform. Also, driven by a dynamic virtual platform, we present results of hardware/software co-simulation and performance analysis for two CPU-FPGA systems.

Th.1.A.111:15add Th.1.A.1 to agenda

Download Th.1.A.1

A Model-Driven Approach for Managing Software Development Processes in the Automotive Industry

Frederic Bessonnier - Renault, France Erich Meier - MethodPark, Germany Theo Lafontan - Altran Toulouse, France

This paper presents a model-driven approach to the software engineering processes. Our solution allows organizations to efficiently respond to transformational challenges while still ensuring reliability, security and safety of their products. In the approach, all software engineering processes are defined in an integrated model that contains standard processes as well as product-line specific variants and project-specific instances. Processes are automatically visualized from the model instead of drawn by hand. Software engineers can view the processes from perspectives that are optimized for their specific context, information requirements, or experience. The processes can be tailored to project-specific requirements and mapped to standards to ensure compliance to Automotive SPICE, ISO 26262, etc. The Renault solution reduces overhead, makes the organizations leaner, and enables them to respond to changes in an agile way.

Th.1.A.211:45add Th.1.A.2 to agenda

Download Th.1.A.2

Introducing Agile Methodology into Advanced Systems Engineering Training

Uwe Kuehne - Airbus Defence and Space, Germany Colin Hamilton - Airbus Defence and Space (retired), Germany Stefan Brueggemann - Airbus Defence and Space, Germany

Agile methods are today very well established in S/W engineering. Because they have proven to be so effective, many companies are now working to extend the agile approach to systems engineering. In Airbus Defence and Space, this is being done with specific training courses supported by coaches in those projects using the agile methodology. In addition to these general measures, Airbus Defence and Space has recently introduced agile methods into its flagship Systems Engineering Qualification course for advanced systems engineers. This program consists of training modules and accompanying (real) projects. In this paper, we will present how we integrated agile methods._x000D_ - in the training modules and_x000D_ - in the projects._x000D_ Furthermore we will explain:_x000D_ - Which agile elements we used and why_x000D_ - What preparations were needed_x000D_ - What experience we gained_x000D_ - Our conclusions and Way Ahead for future SEQ programs

Th.1.A.312:15add Th.1.A.3 to agenda

Download Th.1.A.3
Download Th.1.A.3 presentation

Quality Quantification Applied to Automotive Embedded Systems and Software - Advances with qualimetry science

Yann Argotti - LAAS/CNRS - Renault Software Labs, France Claude Baron - LAAS/CNRS - INSA, France Philippe Esteban - LAAS/CNRS - Université Toulouse III, France Denis Chaton - Renault Software Labs, France

Quality quantification is an unavoidable topic in today daily company life. In this paper, the authors review why quality quantification is critical, what are the main difficulties with the current approaches and highlight the qualimetry approach as the solution. After a state of the art on qualimetry and on quality model concept strengthened with polymorphism, the first steps of their applications to automotive embedded systems and software in Renault are showcased. The results are not only the benefits in quality quantification for complex systems, such as homogeneity, consistency and compatibility, but also the highlighted risks with the changes in versions of quality models in Automotive SPICE and how to define a derivable quality model over electronic control units and vehicle.

Th.1.B.111:15add Th.1.B.1 to agenda

Download Th.1.B.1
Download Th.1.B.1 presentation

Automatic Verification of BPMN Models

Mihal Brumbulli - PragmaDev, France Emmanuel Gaudin - PragmaDev, France Ciprian Teodorov - ENSTA Bretagne, France

Models of complex systems and systems of systems are described with NAF (NATO Architecture Framework) or DoDAF (DoD Architecture Framework). Business Process Model Notation (BPMN) is part of NAF and allows to describe the behavior of the different participants in the model. This notation is used by the French Army and its main suppliers to describe the interactions between participants involved in a mission. It is therefore important the models are correct. The VeriMoB project is a research project financed by the DGA (Direction Générale de l’Armement) which aims at developing a tool that will help users to verify their BPMN models. This tool covers three main aspects: static verification, interactive execution, automatic exploration of the possible scenarios. This paper focuses on the automatic exploration of the model with OBP technology coming from ENSTA Bretagne research lab.

Th.1.B.211:45add Th.1.B.2 to agenda

Download Th.1.B.2

Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites

Silvano Dal Zilio - LAAS-CNRS, France Vincent Mussot - Institute of Research and Technology (IRT) Saint-Exupéry, France Loïc Correnson - CEA, List, Software Safety and Security Lab, France Serge Rainjonneau - Institute of Research and Technology (IRT) Saint-Exupéry, France Yves Bardout - Institute of Research and Technology (IRT) Saint-Exupéry, France Grégoire Scano - Institute of Research and Technology (IRT) Saint-Exupéry, France

We propose a new approach for modelling the functional behaviour of an Earth observation satellite. We leverage this approach in order to develop a safety critical software, a ``telecommand verifier'', that is in charge of checking onboard whether a sequence of instructions is safe for execution. This new service is needed in order to add more autonomy to satellites. To do so, we propose a new Domain Specific Modelling Language and the toolchain required for integration into an embedded software. This framework is based on the composition of deterministic finite state machines with safety conditions, timeouts, and transitions that accept durations as a parameter. It is able to generate code in the synchronous programming language Lustre from a high-level specification of the satellite. This gives a formal way to derive an event-based algorithm simulating the execution of telecommand sequence and, thereupon, a provably correct onboard verifier.

Th.1.B.312:15add Th.1.B.3 to agenda

Download Th.1.B.3
Download Th.1.B.3 presentation

Industrial use of a safe and efficient formal method based software engineering process in avionics

Abderrahmane Brahmi - Airbus Operations SAS, France Mohamed Habib Essoussi - Airbus Operations SAS, France Pascal Lacabanne - Airbus Operations SAS, France Victoria Moya Lamiel - Airbus Operations SAS, Spain Jean Souyris - Airbus Operations SAS, France Marie-Jo Carolus - Airbus Operations SAS, France David Delmas - Airbus Operations SAS, France Famantanantsoa Randimbivololona - Cepresy, France

Abstract: Formal methods have reached industrial efficiency in avionics thanks to the development and deployment of an engineering process for software design and verification processes. It encompasses languages, compilers and formal verification tools in a highly automated workshop, together with adapted methods of use. This engineering process involves functional and non-functional formal verification techniques in a complementary way. It is being applied to the new avionics software products developed at Airbus. Currently, this means that tens of developers have been using the workshop daily since its initial deployment, three years ago. After presenting this engineering process, the main purpose of this paper is to report on its industrial use.

Th.1.C.111:15add Th.1.C.1 to agenda

Download Th.1.C.1
Download Th.1.C.1 presentation

PHYLOG certification methodology: a sane way to embed multi-core processors

Frédéric Boniol - ONERA, France Bouchebaba Youcef - ONERA, France Brunel Julien - ONERA, France Kevin Delmas - ONERA, France Thomas Loquen - ONERA, France Alfonso Mascarenas Gonzalez - ONERA, France Claire Pagetti - ONERA / IRIT-ENSEEIHT, France Thomas Polacsek - ONERA, France Nathanaël Sensfelder - ONERA, France

The PHYLOG project aims at offering a model-based software-aided certification_x000D_ framework for aeronautical systems based on multi/many-core architectures. Certifying such platforms will entail fulfilling the high level objectives of the MCP-CRI/CAST-32A position paper. To reach this general objective, we have defined _x000D_ - a certification framework based on justification patterns to express any argumentation. The idea is to organize any argumentation around structured graphical notations diagrams. _x000D_ - formal and automatic analyses to support the proof of the argumentation. _x000D_ A justification pattern comes with a series of evidences that support the reasoning. Among those evidences, two types of analysis are required by the MCP-CRI: interference and safety analyses. _x000D_ _x000D_ In this paper, we will introduce the certification methodology and apply it partially on the Keystone.

Th.1.C.211:45add Th.1.C.2 to agenda

Download Th.1.C.2
Download Th.1.C.2 presentation

Using Model Checking to Identify Timing Interferences on Multicore Processors

Viet Anh Nguyen - IRT Saint Exupery, France Eric Jenn - IRT Saint Exupery, France Wendelin Serwe - Univ. Grenoble Alpes, Inria, CNRS, France Frederic Lang - Univ. Grenoble Alpes, Inria, CNRS, France Radu Mateescu - Univ. Grenoble Alpes, Inria, CNRS, France

Multicore platforms provide the computing capabilities and the power efficiency required by the complex applications embedded in aeronautical, spatial, and automotive systems. For multiple tasks to run concurrently and in parallel on the different cores, some of the hardware resources provided by the platform ---including buses, caches, and IPs --- are shared between tasks executing concurrently and in parallel on different cores. This sharing may lead tasks to interfere with each other. Therefore, crucial design activities are to identify interferences, and bound the penalty induced by those interferences, as part of the demonstration of compliance of applications to their temporal requirements. A first and conservative approach is to consider that every access to a shared resource leads to an interference. This safe approach is usually too pessimistic to be useful. We propose a less pessimistic approach, which takes into account the actual behavior of the application and the hardware to filter out situations where interferences cannot occur. Our method relies on (i) the behavioral modeling of the applications and their execution platform using the LNT formal language, (ii) the definition of interferences using temporal properties, and (iii) the exploitation of the behavioral model and the temporal properties using the CADP formal verification toolbox. This method is applied to the Infineon AURIX TC275 system-on-chip. Experimental results indicate that our approach is not only safe but also prevents reporting spurious interferences compared to a purely structural analysis.

Th.1.C.312:15add Th.1.C.3 to agenda

Download Th.1.C.3
Download Th.1.C.3 presentation

Formal Modeling and Verification for Timing Predictability

Mihail Asavoae - CEA LIST, France Mathieu Jan - CEA LIST, France Belgacem Ben Hedia - CEA LIST, France

Real-time and embedded systems rely on worst-case timing reasoning to guarantee their timing behaviors. The precision of such approaches depends on how ``analyzable'', from a timing perspective, are these systems. This property is known as timing predictability. In this paper, we look at timing predictability issues through formal methods lenses. More concretely, we address timing predictability claims through formal modeling and verification of both the application and the underlying computer architecture.

Th.2.A.114:00add Th.2.A.1 to agenda

Download Th.2.A.1
Download Th.1.A.1 presentation

Suitability of Time Sensitive Networking for spacecraft industry

Pierre-Julien Chaine - Airbus Defence and Space, France Marc Boyer - Onera, France Claire Pagetti - Onera, France Franck Wartel - Airbus Defence and Space, France

The European spacecraft industry has developed guidelines for generic satellite development known as SAVOIR (Space AVionics Open Interface Architecture). While the current satellites on-board networks implementations are compliant with this standard, their evolution opportunities are strongly limited. New missions and new clients are always more demanding on performance on-board, leading to the conclusion that the satellite embedded network must be upgraded. One opportunity appears with Time Sensitive Networking, an IEEE Ethernet technology capable of supporting both real-time and high-bandwidth traffic. The goal of this paper is to discuss, in a qualitative study, how TSN protocols can help to integrate Quality of Service in new generation satellites.

Th.2.A.214:30add Th.2.A.2 to agenda

Download Th.2.A.2
Download Th.2.A.2 presentation

A new network configuration management architecture for future aircraft systems

Thibault Delmas - Safran Electrical and Power, France Luigi Iannone - Telecom ParisTech, France Bruno Monsuez - ENSTA ParisTech, France Jean-Pierre Garcia - Safran Electrical and Power, France

Aircraft systems are evolving and being enhanced thanks to new design paradigms leveraging on recent technology advances in embedded systems. However, the Integrated Modular Avionics (IMA) model, used in current avionics, has shown important limitations to accommodate such evolution. These new paradigms demand for much more global system modularity than what IMA is able to offer. Such system evolution has as well an impact on the underlying different networks present on aircrafts. In this context, it is mandatory to investigate the kind and the breadth of adaptation networks need in order to cope with new requirements. To this end, this paper we firstly investigate the current aircrafts network configuration and management procedures. It appears that they lack the features, more specifically, the configuration management features, necessary to support these new use cases. We then look at proposals trying to fulfil this features gap. Each of them, while providing parts of the answers, also come with trade-off or insufficiencies that prevent them from fully answering to the new needs. Then, a new network configuration architecture able to cope with the newly defined configuration management requirements is provided. A comparison to the other approaches is presented, so to highlight how the proposed architecture better fulfils long-term evolution requirements while being less complex and more suitable for current configuration procedures than the other proposal. Finally, a simulation of the configuration architecture is done to provide insights on the new proposed features.

Th.2.A.315:00add Th.2.A.3 to agenda

Download Th.2.A.3
Download Th.2.A.3 presentation

Service Oriented Architecture in Automotive

Marc Bellanger - Renault Software Labs, France Edward Marmounier - Renault Software Labs, France

In automotive, software is becoming more and more important because the added value is no longer only in the mechanics of the car but, now, also in the growing features set brought to the driver and its passengers such as driving assistance, entertainment, remote control, data reporting and many others._x000D_ _x000D_ This increasing complexity implies adoption of a SW architecture paradigm that has already be proven in IT and Web development. This paradigm is known as SOA (Service Oriented Architecture). _x000D_ _x000D_ In this paper, we will describe how the SOA has been adapted to automotive constraints and especially describe how Renault introduced the concept through examples._x000D_

Th.2.B.114:00add Th.2.B.1 to agenda

Download Th.2.B.1
Download Th.2.B.1 presentation

Towards Formal Verification of Autonomous Driving Supervisor Functions

Assioua Yasmine - Renault Software Labs, France Ameur-Boulifa Rabea - LTCI, Telecom Paris, Institut polytechnique de Paris, France Guitton-Ouhamou Patricia - Renault Software Labs, France

In the software development lifecycle, errors and flaws can be introduced in the different phases and lead to failures. Establishing a set of functional requirements helps producing safe software. However, ensuring that the (being) developed software is compliant with those requirements is a challenging task due to the lack of automatic and formal means to lead this verification. In this paper, we present our approach that aims at analysing a collection of automotive requirements by using formal methods. The proposed approach for formal verification is evaluated by the application to supervisor functions of the autonomous driving (AD) system, the system in charge of self-driving.

Th.2.B.214:30add Th.2.B.2 to agenda

Download Th.2.B.2
Download Th.2.B.2 presentation 1
Download Th.2.B.2 presentation 2

ASTERIOS Checker: A Verification Tool for Certifying Airborne Software

Amira Methni - Krono-Safe, France Emmanuel Ohayon - Krono-Safe, France Francois Thurieau - Safran Electronics & Defense, France

As the number of embedded systems has grown regularly over the past decades, the development and certification costs of safety-critical software has increased accordingly. For the aeronautics industry, certification activities are covered by DO-178C, which provides guidance for developing airborne software and its companion document DO-330 covers the qualification of tools used for the development of such software. In this paper, we present ASTERIOS, a solution for the design, generation and execution of safety critical real-time applications then we present the certification strategy we advocate for systems developed using our technology. This strategy relies on the use of an automated verification tool called ASTERIOS Checker, qualified in accordance with DO-330. This paper presents the technology behind the code generation engine of ASTERIOS and the verification activities automated by ASTERIOS Checker. It shows how the use of such an automated, qualified tool enables to benefit from design abstractions and relatively complex code generation engines while developing certified systems at the highest level of certification.

Th.2.B.315:00add Th.2.B.3 to agenda

Download Th.2.B.3
Download Th.2.B.3 presentation

Data Consistency Testing in Automotive Multi-Core Applications - towards systematic requirement elicitation

Ralph Mader - Vitesco Technologies GmbH, Germany Stefan Resmerita - University of Salzburg and Chrona.com, Austria Lucian Bara - Vitesco Technologies GmbH, Romania Wolfgang Pree - Chrona.com, Austria Anton Pölzleitner - University of Salzburg and Chrona.com, Austria

Today multi-core micro-controllers are widely used in automotive applications. Increased performance requirements and the need for speed up increasingly require the distribution of software across cores. Independent of what type of software is used, legacy or AUTOSAR-Classic, ensuring data consistency is fundamental for the proper execution of the functionality. For performance reasons data consistency shall not be over- specified, which could result in a too high CPU load and memory allocation due to a massive usage of semaphores. For this purpose, AUTOSAR-Classic provides the possibility to specify consistency requirements for optimizations. But how can the crucial consistency requirements be identified? Today this is mainly done by a design review of the software module with respect to its input variables. In this paper we propose a method which allows the identification of consistency requirements for a module in a formal way. It is based on the identification of so-called problematic access patterns for the input data which are then enforced in the Software In the Loop (SIL) in a dynamic stress test. The results of the module are checked against the expected test vectors. In case such problematic access patterns create a violation of data consistency, that is, a deviation from the expected test result, the generation of a corresponding consistency requirement is indicated to the developer. The method can be integrated into an existing test environment for model based development.

Th.2.C.114:00add Th.2.C.1 to agenda

Download Th.2.C.1
Download Th.2.C.1 presentation

Early validation of satellite COTS-on-board computing systems

Philippe Cuenot - IRT Saint Exupéry, France Julien Deantoni - Université Cote d’Azur, I3S/INRIA Kairos, France Amin Ouestali - IRT Saint Exupéry, France Paul Bouche - IRT Saint Exupéry, France Robert De Simone - INRIA Kairos, France

The competitive market of nano and micro satellites opens perspectives for use of COTS (Commercial Off-The-Shelf) electronic components. Current modular electronics design for embedded On-Board Computing systems (OBC) is being challenged by the integration of flexible Systems on Chip (SoC). The deployment of generic avionics and user/payload functionalities on these components is becoming increasingly complex, while Quality of Service must remain compliant with demanding requirements. It is therefore most important to estimate/evaluate those properties as early as possible, regarding a given application’s deployment on a given COTS-based architecture. Model Based System Engineering (MBSE), while a leading practice in architecture description, may still require further study on its use for early evaluation, especially regarding analysis of emerging behaviors and qualitative model based mapping of applicative functions onto architectural platform. In this paper, we present methods to enhance MBSE design, helping the designer in evaluating candidate mappings and design choices by providing concrete quality measures. We focus on two aspects that were identified as critical in the ATIPPIC IRT project: first, the cost and conflicts in data communications in on-board and peripheral interconnects, which has a bottleneck impact on mapping choices second, the availability of functions in case of resource failures (from solar radiations), to validate fault-mitigation techniques and estimate the (un)availability of the OBC system. We illustrate the approach on a simplified satellite model, abstracted from a design conceived in the ATIPPIC IRT project.

Th.2.C.214:30add Th.2.C.2 to agenda

Download Th.2.C.2
Download Th.2.C.2 presentation

LAMP: A new model processing language for AADL

Pierre Dissaux - Ellidiss Technologies, France

Increasing use of Model Driven Engineering in industry implies the need to elaborate efficient solutions for model processing. Typical model processing activities address early verification (model exploration, constraints enforcement, static analysis, interfacing with verification languages and tools) as well as production (automatic generation of documentation, code or test cases). Most of the time, model processing languages are closely associated with the modelling language they are working on. The AADL community has also identified the need to define processing languages that can leverage the intrinsic strong semantics of this modelling approach. Dedicated languages like REAL , LUTE or RESOLUTE have been developed in that purpose. This paper presents an alternate original and powerful model processing language that can be directly embedded within AADL models. Based on the use of the Prolog language and the LMP framework, this new model processing language is called LAMP, standing for Logic AADL Model Processing. LAMP is implemented in the AADL Inspector tool and is composed of three main components: - LAMP Annexes located in the end user AADL source text, where processing goals and rules can be defined. - The LAMP Standard Library providing a list of predefined utility rules and accessors to the AADL declarative and instance models. - A LAMP Checker plugin that assembles Prolog facts bases and rules bases together, runs the Prolog interpreter and shows the results in a console or a file. Examples of use of LAMP rules are provided in the paper, as varied as model exploration, static analysis, end to end flow analysis, fault tree generation or security rules.

Th.2.C.315:00add Th.2.C.3 to agenda

Download Th.2.C.3
Download Th.2.C.3 presentation

Engineering Railway Systems using an Architecture-Centric Process Supported by AADL and ALISA: an Experience Report

Paolo Crisafulli - IRT SystemX, France Dominique Blouin - Telecom Paristech, France Francoise Caron - Eiris Conseil, France Cristian Maxim - IRT SystemX, France

The increasing automation of transportation systems has contributed to the emergence of so-called cyber-physical systems (CPS): computation based systems that combine computing devices, sensors, actuators and networking, designed to monitor and control physical feedback loops, often mutually dependent. To cope with this complexity, engineering teams require model based tools. Early integration and verification, reuse of existing models, requirements traceability and support of an incremental process could be ensured trough modeling. Above all, the modeling languages must be expressive enough to capture all aspects necessary to perform the virtual verifications with the required confidence degree. Our experiment results in a showcase of how AADL and ALISA can support an agile architecture-centric development process for a typical embedded system in the railway domain: continuous verification maintains the design within the solution space shaped by the set of requirements, while KPIs computation and charting qualify its evolution and alternatives over time, in terms of performance.

Download Th.Panel 1 presentation

Th.3.A.117:00add Th.3.A.1 to agenda

Download Th.3.A.1
Download Th.3.A.1 presentation

Profiling and optimization of Deep Neural Networks for embedded automotive applications

Eric Perraud - Renault Software Labs, France Jean-Marc Gabriel - Renault Software Labs, France Loïc Cordone - Renault Software Labs, France

Until now, an automotive Electronic Control Unit has executed a single function and an automotive function has been implemented on a single ECU. This bijective mapping between one ECU and one automotive function has allowed a simple definition of the product. But this has become a bottleneck for new automotive functionalities. Recently, Deep Neural Network (DNN) algorithms have shown tremendous progress and the question of their integration into vehicles begins to arise. These DNN algorithms usually come from other industries with quasi-infinite hardware resources (very powerful server CPUs, huge amount of available memory, etc.). The hardware resource usage of such algorithms can’t easily be predicted because they have been developed with a framework (TensorFlow, PyTorch, etc.) where the DNN algorithm developer does not control the allocated memory, the scheduling of operations, neither the level of parallelization. Hence it is needed to profile these SW functionalities before integrating them in an ECU. We can foresee mutiple types of deep learning algorithms coming in automotive applications: Fully-Connected DNN (FC-DNN), Convolutional Neural Networks (CNN) or Recurrent Neural Network (RNN). In this paper, we investigate an approach combining deep learning profilers and deep learning compilers to: - Assess the inference latency, - Determine where the optimization effort (if needed) should focus, - Compile the model for a fast and lightweight inference on the target ECU. As an example, CNN typically address Computer Vision applications such as object detection and classification. When the framework converts the CNN graph into executable code for a given target CPU, the generated code may not be optimal from an execution time or CPU load perspective. Therefore, if the CPU load of such CNN algorithms exceeds the CPU budget which can be allocated, an optimization effort shall be done. Recent research works claim to do these optimizations automatically, for every architecture (CPU, GPU, FPGA), without changing the CNN graph. We propose an evaluation of one of these so-called Deep Learning Compilers : TVM. We show that the inference time can be divided in a 2x ratio for the well-known Mobilenet-SSD algorithm (which is a CNN), thereby reducing the hardware constraints on the embedded ECU and making their integration in automotive applications easier. We even have measured that the inference time can be divided in a 4x ratio for a RNN, using such deep learning compiler. Therefore, while deep learning profiling allows to identify bottlenecks of the DNN execution, deep learning compiler like TVM allows to optimize the model for a fast and lightweight inference on a diversity of hardware. It also allows a complete separation between the DNN design and its porting on embedded systems.

Th.3.A.217:30add Th.3.A.2 to agenda

Download Th.3.A.2
Download Th.3.A.2 presentation

Capability to Embed Deep Neural Networks: Study on CPU Processor in Avionics Context

Sergei Chichin - Airbus S.A.S., France Marc Brundler - AUSY, France Dominique Portes - Airbus S.A.S., France Victor Jegu - Airbus S.A.S., France

Deep Neural Networks (DNN) are rapidly gaining popularity due to their ability to provide technically and economically viable solutions to some complex tasks, that are currently performed by humans. Despite of additional challenges related to the certification process, the avionics industry is likely to adopt this new technology in the near future, starting from low Design Assurance Levels (DAL) and moving towards safety-critical systems. In order to deploy a neural network on an aircraft, it is crucial to be able (i) to guarantee a safe deterministic behavior of the intended function as well as (ii) to ensure sufficiency of computational resources for real-time execution. While there is a growing interest in academia and industry to the safety implications of Artificial Intelligence, the capability to embed such algorithms in avionics equipment did not gain sufficient attention. Although some vendors provide specialized hardware and the associated frameworks for an efficient execution of such algorithms, they are not designed with avionics constraints in mind and do not provide a sufficient level of guarantees to be accepted by the authorities. Therefore, in this work we investigate our capability to embed a DNN on a recent CPU processor. In particular, we aim to provide an efficient implementation of a DNN inference algorithm on the target hardware, while considering its compatibility with avionics certification requirements. Finally, we automate the DNN code generation from TensorFlow exported models and study experimentally the impact of DNN’s architecture on the execution time and the consumed resources.

Th.3.B.117:00add Th.3.B.1 to agenda

Download Th.3.B.1
Download Th.3.B.1 presentation

Safety Annex for the Architecture Analysis and Design Language

Danielle Stewart - University of Minnesota, United States Jing Liu - Collins Aerospace, United States Darren Cofer - Collins Aerospace, United States Mats Heimdahl - University of Minnesota, United States Michael Whalen - University of Minnesota, United States Michael Peterson - Collins Aerospace, United States

Model-based development tools are increasingly being used for system-level development of safety-critical systems. Architectural and behavioral models provide important information that can be leveraged to improve the system safety analysis process. Model-based design artifacts produced in early stage development activities can be used to perform system safety analysis, reducing costs and providing accurate results throughout the system life-cycle. In this paper we describe an extension to the Architecture Analysis and Design Language (AADL) that supports modeling of system behavior under failure conditions. This Safety Annex enables the independent modeling of component failures and allows safety engineers to weave various types of fault behavior into the nominal system model. The accompanying tool support uses model checking to propagate errors from their source to their effect on top-level safety properties without the need to add separate propagation specifications. Our tools are also able to compute minimal cutsets for these errors to produce faults trees familiar to safety engineers and certification authorities. We describe the Safety Annex, illustrate its use with a representative example, and discuss and demonstrate the tool support enabling an analyst to investigate the system behavior under failure conditions.

Th.3.B.217:30add Th.3.B.2 to agenda

Download Th.3.B.2
Download Th.3.B.2 presentation

On the safety assessment of RPAS safety policy

Diego Couto - ONERA, France Kevin Delmas - ONERA, France Xavier Pucel - ONERA, France

Remotely Piloted Aircraft Systems (RPASs) should become shortly mainstream to meet the operational requirements of emerging applications such as autonomous transport or infrastructure monitoring. The integration of these systems in the airspace creates new issues, especially concerning safety. The variety of operational contexts where RPAS are involved defeats the safety assessment processes used for decades for large civil aircrafts. One of the major issues is the lack of standardisation of RPAS safety policies. We claim that including the safety policy during safety assessment is one of the prominent challenges for a safe integration of the RPAS in the airspace. Hence, we provide a formal modelling and analysis framework dedicated to the safety assessment of RPAS safety policies.

Th.3.C.117:00add Th.3.C.1 to agenda

Download Th.3.C.1
Download Th.3.C.1 presentation

Using SPARK to Ensure System to Software Integrity

Tonu Naks - AdaCore, Estonia M. Anthony Aiello - AdaCore, United States S. Tucker Taft - AdaCore, United States

This paper describes work in progress on a workflow that supports consistent property-preservation proofs from early stages of system requirement specifications down to software requirements and final implementation. This workflow, called System-to-Software Integrity (SSI), demonstrates that the implemented software satisfies constraints defined in system requirements. In this paper, we demonstrate two important building blocks of this workflow. First, SysML to Simulink translation, which translates system level property specifications to Simulink where it is easy to perform design of the control software. Second, Simulink to SPARK translation, which supports both checking the consistency of system-level property specifications as well as verification of property preservation in the software design. The approach is demonstrated on a simple example of a car cruise control simulator.

Th.3.C.217:30add Th.3.C.2 to agenda

Download Th.3.C.2
Download Th.3.C.2 presentation

Practical Application of SPARK to OpenUxAS

M. Anthony Aiello - AdaCore Technologies, United States Claire Dross - AdaCore, France Pat Rogers - AdaCore, United States Laura Humphrey - Air Force Research Laboratory, United States James Hamil - LinQuest Corporation, United States

This paper presents initial, positive results from using SPARK to prove critical properties of OpenUxAS, a service-oriented software framework developed by AFRL for mission-level autonomy for teams of cooperating unmanned vehicles. Given the intended use of OpenUxAS, there are many safety and security implications however, these considerations are unaddressed in the current implementation. AFRL is seeking to address these considerations through the use of formal methods, including through the application of SPARK, a programming language that includes a specification language and a toolset for proving that programs satisfy their specifications. Using SPARK, we reimplemented one of the core services in OpenUxAS and proved that a critical part of its functionality satisfies its specification. This successful application provides a foundation for further applications of formal methods to OpenUxAS.

Download Th.Special Focus Session presentation