We.1.A.110:00add We.1.A.1 to agenda

Download We.1.A.1
Download We.1.A.1 presentation

Software-Only Semantic Diverse Redundancy for High-Integrity AI-Based Functionalities

Martí Caro - Barcelona Supercomputing Center, Spain Axel Brando - Barcelona Supercomputing Center, Spain Jaume Abella - Barcelona Supercomputing Center (BSC), Spain

Dual (DMR) and Triple Modular Redundancy (TMR), often with some form of diversity, are used in safety-critical systems to realize those functionalities at the highest integrity level providing fault detection and/or tolerance capabilities. Redundant executions are intended to provide bit-level identical results and, upon any mismatch, an error is assumed and recovery actions taken as needed. In this paper, we note that many emerging AI-based functionalities are intrinsically stochastic (e.g., camera-based object detection), and hence, their correctness must be judged semantically, with room for variations across correct outcomes (e.g., confidence must be above a given threshold). Building on this observation, we propose strategies to create DMR and TMR implementations of AI-based functionalities that bring not only fault tolerance against random hardware faults, but also against AI model inaccuracies. Those strategies, which can be realized with software-only means and ported to virtually any computing platform, build on input data modifications affecting the inference computations, but not the expected semantic output (e.g., introducing some limited random noise in the input data).

We.1.A.210:30add We.1.A.2 to agenda

Download We.1.A.2
Download We.1.A.2 presentation

Formal description of ML models for unambiguous implementation

Adrien Gauffriau - Airbus, France Iryna De Albuquerque Silva - ONERA, France Claire Pagetti - ONERA, France

Implementing deep neural networks in safety critical systems, in particular in the aeronautical domain, will require to offer adequate specification paradigms to preserve the semantics of the trained model on the final hardware platform. In this extended abstract, we briefly sketch how to formally represent neural networks with the NNEF format. We show that NNEF semantic is incomplete and we propose some principles to extend the semantics in order to have a non ambiguous description.

We.1.B.110:00add We.1.B.1 to agenda

Download We.1.B.1
Download We.1.B.1 presentation

A Refinement Method for Interference Analysis using the PHYLOG Modeling Language

Guillaume Brau - Institut de Recherche Technologique Saint-Exupéry, France Eric Jenn - Institut de Recherche Technologique Saint-Exupéry, France Emmanuel Courty - Liebherr-Aerospace, France Kevin Delmas - ONERA, France Frédéric Boniol - ONERA, France

Temporal interference may occur in multicore processor systems due to tasks running in parallel competing for shared resources such as buses or memories. This paper presents a model-based interference analysis based on the PHYLOG framework that intends to help in the certification process of multicore aeronautical systems. As PHYLOG does not define a clear modeling method, a refinement approach is proposed to model the system using the PHYLOG Modeling Language (PML). Our objective is to define a process that enables to build a model that is both precise and reliable so that analysis results are sound. The approach is finally validated on an industrial use case from the aerospace domain.

We.1.B.210:30add We.1.B.2 to agenda

Download We.1.B.2
Download We.1.B.2 presentation

Kryptonite++: Localizing Program Interference on Multi-core Embedded Systems

Nikhilesh Singh - IIT Madras, India Karthikeyan Renganathan - IIT Madras, India Chester Rebeiro - IIT Madras, India Jithin Jose - Vitesco Technologies, India Ralph Mader - Vitesco Technologies, Germany

In recent years, the adoption of multi-core hardware has increased manifold in various embedded systems domains to address cost and power constraints. In order to ensure safety of real-time applications, it is critical to determine the worst-case interference from other programs. Further, improving the interference behavior of programs requires the knowledge of program regions that are susceptible to interference. Existing solutions tend to overestimate the interference, while pinpointing interference hotspots remains an open problem. In this paper, we present Kryptonite++, a framework to synthesize the worst-case program interference environment for a given program on a multi-core hardware. Kryptonite++ builds the maximally interfering environment using small code gadgets that are designed to hammer specific hardware modules. To arrange these gadgets, we use a greedy approach followed by a Reinforcement Learning algorithm. Kryptonite++ finally analyzes the interference patterns and the executed instructions to pinpoint the hotspots of interference in the program. We demonstrate Kryptonite++ on the automotive grade Infineon AURIX TC399 processor with a wide range of programs.

We.1.C.110:00add We.1.C.1 to agenda

Download We.1.C.1
Download We.1.C.1 presentation

An Evaluation Bench for the Exploration of Machine Learning Deployment Solutions on Embedded Platforms

Eric Jenn - IRT Saint Exupery, France Floris Thiant - IRT System X, France Theo Allouche - ATOS, France Halima Bouzidi - Université Polytechnique Haut de France, France Ramon Conejo-Laguna - IRT Saint Exupery, France Omar Hlimi - IRT Saint Exupery, France Cyril Louis-Stanislas - VIVERIS, France Christophe Marabotto - IRT Saint Exupery, France Smail Niar - Université Polytechnique Haut de France, France Serge Tembo-Mouafo - IRT Saint Exupery, France Philippe Thierion - Renault Software Labs, France

Finding the most efficient deployment of a Machine Learning (ML) model can hardly be done on the unique basis of available documentation. In practice, it requires setting up and exploring multiple combinations of ML tools and hardware targets, running series of experiments, and evaluating pertinent parameters (inference latency, memory usage, etc.). All these operations are complex, sometimes tedious, and always time consuming. Therefore, in order to facilitate this Design Space Exploration process, we propose an evaluation bench that (i)~integrates the necessary software and hardware resources (tools, boards) to deploy a varieties of ML models, and (ii) provides a uniform and abstract API to exercise and evaluate multiple deployment solutions. This paper defines more precisely the end-users needs, describes the architecture of the bench and illustrates its application on use cases.

We.1.C.210:30add We.1.C.2 to agenda

Download We.1.C.2
Download We.1.C.2 presentation

Multi-core WCET Analysis Using Non-Intrusive Continuous Observation

Daniel Kästner - AbsInt GmbH, Germany Gernot Gebhard - AbsInt GmbH, Germany Markus Pister - AbsInt GmbH, Germany Simon Wegener - AbsInt GmbH, Germany Christian Ferdinand - AbsInt GmbH, Germany Alexander Weiss - Accemic Technologies GmbH, Germany Albert Schulz - Accemic Technologies GmbH, Germany Martin Sachenbacher - Accemic Technologies GmbH, Germany Martin Leucker - University of Lübeck, Germany

For safety-relevant real-time applications, worst-case execution time (WCET) bounds have to be determined in order to demonstrate deadline adherence. For timing predictable microprocessors, worst-case execution time guarantees can be computed by static WCET analysis. Hybrid WCET analysis is a solution for covering effects from accesses to interference channels of multi-core processors. In this article we present a seamless approach for hybrid WCET analysis that tightly couples the tools TimeWeaver and CEDARtools. We will describe the underlying concepts, illustrate the tool workflow, and discuss the application of our approach to meet the timing requirements of the EASA AMC 20-193 guidance.

We.4.A.115:00add We.4.A.1 to agenda

Download We.4.A.1
Download We.4.A.1 presentation

Digital twin for embedded software. State of art in industry and deployment at Renault Group for powertrain

Jean-Marie Quelin - AMPERE (Renault Group), France Christian Becker - DSPACE Gmbh, Germany Salim Bouabdallah - Dspace France, France

Abstract — Virtualization is a technology that has evolved over the last ten years. The solution reaches a level of feature that fits to the new needs of the automotive industry. The paper presents the state of the art and the return on experience of AMPERE ePowertrain Team by showing the deployment of SIL and HIL on several use cases.

We.4.A.215:30add We.4.A.2 to agenda

Download We.4.A.2
Download We.4.A.2 presentation

Towards safe obstacle detection for autonomous train operation: Combining track and switch detection neural networks for robust railway ego track detection

Philipp Jass - HTW Berlin, Germany Carsten Thomas - HTW Berlin, Germany Tina Hiebert - HTW Berlin, Germany Gustav Plettig - HTW Berlin, Germany

Similar to autonomous driving on the road, automated and autonomous train operation also offers many advantages. These include relieving the burden on train drivers, as well as a possible increase in line capacity or the redevelopment of previously unprofitable sections of line. One of the most important tasks of an autonomous train control system is to monitor the surroundings and, above all, the route to be traveled. This must be continuously monitored for possible obstacles in the train's path, just as a human train driver does. In order to perform this task, sensors are required that record data about the train's surroundings. Such sensors in autonomous systems are usually cameras, radar or lidar sensors. To detect obstacles on the track, the critical zone must first be identified. For trains, this area is called the clearance gauge and describes the space that the train occupies when traveling on a track. In complex scenes with switches, the section of track that the train travels through depending on the status of the switches must be determined. This is referred to as the ego track. This paper presents an image-based approach for embedded on-board ego track determination, combining track and switch information in order to achieve a more robust ego track prediction.

We.4.A.316:00add We.4.A.3 to agenda

Download We.4.A.3
Download We.4.A.3 presentation

Partially trustworthy action planning thanks to an easily certified plan validator

Jean-Louis Dufour - SAFRAN Electronics & Defense, France

Action planning is the second obstacle (after environment perception) on the path to trustworthy autonomous systems. An action planner is so complex that certifying it would be astronomically expensive. So it will be necessary to associate it with a plan validator responsible for checking plan correctness, to whom the full weight of certification will be transferred. The contribution of this paper is the simple observation of the unexpected proximity between the PDDL planning language and the Scade synchronous language. From the technical point of view, this proximity allows a simple translation from PDDL to a Scade model of this plan validator. From the process point of view, if PDDL is accepted as a software specification language, it greatly facilitates validator certification. The two models accept the same plans when all the variables have finite domains, but this is no longer true with an integer-valued variable, and we will sketch a way to deal with this problem.

We.4.B.115:00add We.4.B.1 to agenda

Download We.4.B.1

Design by contract formal verification for automotive embedded software robustness

Vassil Todorov - Stellantis, France Alin Mihalache - Stellantis, France Azzedine Azil - Stellantis, France Armando Hernandez - Stellantis, France

abstract of regular paper: Preventing software failures is of high importance for the safety or security related embedded software. Among the most critical defects are runtime errors such as buffer overflows, accessing data outside the allocated memory, divide by zero or data races. The ISO 26262 functional safety standard for road vehicles requires to use static code analysis for unit and integration verification but this method is generally unsound and cannot guarantee exhaustiveness i.e., some defects can still be present in the code. In 2018, ISO 26262 was updated and introduced a recommendation for static code analysis based on abstract interpretation. Abstract interpretation is a formal method which means that it can guarantee mathematically the absence of runtime errors in an exhaustive manner. To be exhaustive it uses approximation algorithms that can bring a huge number of false alarms. For this reason, this method is not largely deployed in the automotive industry today. In this paper, we propose to introduce a design by contract approach to provide the abstract interpretation static analyzer additional information for the input variables and the parameters to increase its precision and significantly reduce the number of false alarms. For the outputs, we use the contracts to prove they are compliant to the ranges defined by the specification. We automated the procurement of contracts from different sources: a database defining the software architecture, CAN network signals definition or the AUTOSAR ARXML interface definition files. Finally, we provide the results obtained for our production code for analyses with or without contacts and show how effective is their use.

We.4.B.215:30add We.4.B.2 to agenda

Download We.4.B.2
Download We.4.B.2 presentation

Automated Test Suite Augmentation using Language Models: Applying RAG to Improve Robustness Verification

Adam Mackay - QA-Systems, United Kingdom

Description of the Research Work in Progress We are exploring the application of cutting-edge AI techniques like large language models and retrieval augmented generation to automate test case generation focused on robustness verification for safety-critical embedded systems. Initial results from leveraging GPT-4 and integrating RAG across software repositories unveil a promising pathway to enhance test thoroughness and unveil defects while achieving high coverage standards. Ongoing work is refining these methods and expanding capabilities by adopting advanced models like Llama 2 and optimizing them for embedded systems projects, with the overarching goal of boosting reliability through automated testing. Short Positioning with Regards to the State of the Art While test automation has made strides, manually authoring test cases, especially for robustness verification, remains demanding. Recent breakthroughs in AI like large language models enable new pathways for automated testing. This research pioneers the application of models like GPT-4 and techniques like retrieval augmented generation to augment test suites for critical systems. By harnessing AI's generative capabilities and integrating relevant contextual data, this work pushes automated testing into new realms of effectiveness and efficiency. Short Report of the Current Results and Further Plans Initial results demonstrate this approach can surpass human-written tests in thoroughness and defect detection for embedded projects, while maintaining requirements linking for standards like DO-178C. Further plans involve adopting advanced models like Llama 2, optimizing them for embedded systems, and expanding RAG across requirements and design documents to enable test case derivation earlier in development. Through iterative refinement, this research continues pursuing enhanced reliability via increasingly capable AI-driven testing.

We.4.B.316:00add We.4.B.3 to agenda

Download We.4.B.3
Download We.4.B.3 presentation

Mixing tests and mathematical analysis - A launcher use case

David Lesens - Ariane Group, France Mathilde Ducamp - Ariane Group, France Philippe Ranoarivony - ArianeGroup, France

This paper shows on a case study (launcher sequence) how simple semi-formal methods and tools (SysML modelling, Domaine Specific Language, Simplex algorithm) can be used to improve the development and the validation of industrial systems without using complex formal methods which are sometimes difficult to manage by engineers.

We.4.C.115:00add We.4.C.1 to agenda

Download We.4.C.1
Download We.4.C.1 presentation

Large legacy systems design maintainability through modeling

Mohamed-Habib Essoussi - Airbus Operations S.A.S, France Paul Vivot - Airbus Operations S.A.S, France Lucas Deloye - SII, France Davi Henrique Sousa Pinto - Airbus Operations GmbH, France

Model-Based System Engineering (MBSE) and particularly Model-Based Product Line Engineering (MBPLE) now stands as the new standard for systems engineering at Airbus Group. Indeed, the Airbus MBSE Architecture Framework (R-MOFLT) and its feature-based product line engineering framework extension (MBPLE4MOFLT) are widely deployed on Research & Technology projects. This paper tackles the applicability of such enablers to large legacy systems. As such, it outlines a proof of concept on redesigning a legacy system using MBPLE4MOFLT as a new product line based on several in-service variants definitions that have been designed over the last four decades following document-based ways of working. As such, the interoperability between these ways of working and the new digital assets is essential to achieve this migration on one side and, once migrated, to ensure backwards compatibility with the official process, on the other side. To this aim, besides using existing data hubs between Cameo Systems Modeler and Rational Doors, the Airbus MBSE SysML profile has been extended with further customizations to fit the new product line design golden rules. Wizards are also proposed to ease authoring and impact analysis. Finally, a new plugin has been developed to automate the variability propagation throughout variant assets and to ensure consistency between the variability handled with MBPLE4MOFLT and the requirements applicabilities handled in Rational Doors.

We.4.C.215:30add We.4.C.2 to agenda

Download We.4.C.2
Download We.4.C.2 presentation

Coupling optimization using Design Structure Matrices (DSM) and Genetic Algorithm

Sébastien Dubé - Samares-Engineering, France Mirna Ojeda - Samares-Engineering, France Jean-Marie Gauthier - IRT Saint-Exupery, France

This article seeks to contribute to a nuanced understanding of the integration of Design Structure Matrix(DSM) [1] and genetic algorithms in the context of Cyber-Physical Systems modelling. By examining coupling minimization as a critical aspect of advanced systems engineering practices, we aim to provide a scholarly exploration, blending theoretical insights with practical applications. The objective is to equip systems architects with analytical tools integrated within their Model Based Systems Engineering (MBSE) environment for exploring the design space of component interactions, facilitating the identification of optimal system architectures.

We.4.C.316:00add We.4.C.3 to agenda

Download We.4.C.3
Download We.4.C.3 presentation

Specializing SysMLv2 for Real-Time Safety- Critical Systems – an Experiment with AADLv2

Jerome Hugues - CMU/SEI, United States Pierre Dissaux - Ellidiss Technologies, France

The future release of OMG SysMLv2 provides a new set of foundational layers to support engineering activities of a large set of systems. SysMLv2 relies on a restricted set of concepts combined with a large library to define building blocks for designing systems. This approach makes it possible to define domain-specific libraries that enrich or specialize SysMLv2 elements. In this paper, the authors show how to build one such specialization for real-time safety-critical systems. Starting from the SAE AADL language elements, we show how to a) extend SysMLv2 constructs with AADL ones, and b) propose guidelines to represent AADL static and dynamic semantics. This development serves as a illustration of SysMLv2 extension capabilities. It also addresses a recurring concern of specializing MBSE for domain-specific engineering activities, ranging from design activities to V&V.

We.5.A.117:00add We.5.A.1 to agenda

Download We.5.A.1
Download We.5.A.1 presentation

Certified ML Object Detection for Surveillance Missions

Mohammed Belcaid - CSGROUP, France Eric Bonnafous - CSGROUP, France Louis Crison - CSGROUP, France Christophe Faure - CSGROUP, France Eric Jenn - IRT Saint Exupery, France Claire Pagetti - Onera, France

In this paper, we present the development process of a drone detection system involving a machine learning object detection component. Focus is placed on performance objectives and provision of evidences required for certification. Our approach follows the preliminary recommendations proposed by the Airworthiness Certification Authorities to be consolidated and published in the ARP 6983 standard.

We.5.A.217:30add We.5.A.2 to agenda

Download We.5.A.2
Download We.5.A.2 presentation

How to design a dataset compliant with a ML-based system ODD?

Cyril Cappi - SNCF, France Noémie Cohen - Airbus, France Mélanie Ducoffe - Airbus, France Christophe Gabreau - Airbus, France Laurent Gardes - SNCF, France Adrien Gauffriau - Airbus, France Jean-Brice Ginestet - DGA, France Franck Mamalet - IRT Saint Exupéry, France Vincent Mussot - IRT Saint Exupéry, France Claire Pagetti - ONERA, France David Vigouroux - IRT Saint Exupéry, France

This paper focuses on a Vision-based Landing task and presents the design and the validation of a dataset that would comply with the Operational Design Domain (ODD) of a Machine-Learning (ML) system. Relying on emerging certification standards, we describe the process for establishing ODDs at both the system and image levels. In the process, we present the translation of high-level system constraints into actionable image-level properties, allowing for the definition of verifiable Data Quality Requirements (DQRs). To illustrate this approach, we use the Landing Approach Runway Detection dataset which combines synthetic imagery and real footage, and we focus on the steps required to verify the DQRs. The replicable framework presented in this paper addresses the challenges of designing a dataset compliant with the stringent needs of ML-based systems certification in safety-critical applications.