The certification of safety-critical systems requires amongst other things understanding the underlying hardware platform, and its use in the context of the system. At the processor level, it means that the designer must understand in detail the behaviour of a core executing a program. Many approaches rely on capturing such knowledge in an abstract model of the core. A crucial question is then does the model correctly represent the processor? and how can the designer prove such correctness? In this paper, we propose a methodology to build a core model, taking solely into account the memory accesses, and to validate the resulting model with associated stressing benchmarks.

The resource-constrained environment and the certification requirements underlying embedded safety-critical real-time systems impose an adapted development process for software applications. In this work, we propose an efficient and traceable implementation of an existing blocked general matrix multiplication (GEMM) algorithm. We target time-predictability in a COTS processor with single-instruction multiple-data (SIMD) extensions. We provide a set of rules for tuning the algorithm parameters and predict with precision its number of memory accesses and cache misses, which paves the way for a static WCET analysis. Our experiments show that time-predictability comes at the cost of a performance degradation of only 2.54% on average. Moreover, tuning the parameters allows for reducing cache misses by up to 60% in certain parts of the algorithm.

In this paper, we conduct a comparison of the existing formal methods for verifying the safety of cyber-physical systems with machine learning based controllers. We focus on a particular form of machine learning based controller, namely a classifier based on multiple neural networks, the architecture of which is particularly interesting for embedded applications. We compare both exact and approximate verification techniques, based on several real-world benchmarks such as a collision avoidance system for unmanned aerial vehicles.

Architectures used in safety critical systems have to pass certain certification standards, which require sufficient proof that they will behave as expected. Multi-core processors make this challenging by featuring complex interactions between the tasks they run. A lot of these interactions are made without explicit instructions from the program designers. Furthermore, they can have strong negative impacts on performance (and potentially affect correctness). One important such source of interactions is cache coherence, which speeds up operations in most cases, but can also lead to unexpected variations in execution time if not fully understood. Architecture documentations often lack details on the implementation of cache coherence. We thus propose a strategy to ascertain that the platform does indeed implement the cache coherence protocol its user believes it to. We also apply this strategy to the NXP QorIQ T4240, resulting in the identification of a protocol (MESIF) other than the one this architecture’s documentation led us to believe it was using (MESI).

Tasks in modern multi-core real-time systems share data and communicate among each other. Nonetheless, the majority of published research in real-time systems either assumes that tasks do not share data or prohibits data sharing by design. Only recently, some works investigated solutions to address this limitation and enable data sharing; however, we find these works to suffer from severe limitations. In particular, approaches that bypass private caches to avoid coherence interference altogether suffer from significant average-case performance degradation. On the other hand, proposed predictable cache coherence protocols increase the worst-case memory latency (WCL) quadratically due to coherence interference. In this paper, by carefully analyzing the scenarios that lead to high coherence interference, we make the following observation. A protocol that distinguishes between non-modifying (read) and modifying (write) memory accesses is key towards reducing the effects of coherence interference on WCL. Accordingly, we propose DISCO, a discriminative coherence solution that capitalizes on this observation to balance average-case performance and WCL. This is achieved by disallowing modified data in private caches, and hence, the significant coherence delays resulting from them are avoided. In addition, DISCO achieves high average performance by allowing tasks to simultaneously read shared data in the private caches. Moreover, if the system supports the distinction between private and shared data, DISCO further improves average performance by allowing for the caching of private data in cores' private caches regardless of whether it is modified or not. Our evaluation shows that DISCO achieves 7.2× lower latency bounds compared to the state-of-the-art predictable coherence protocol. DISCO also achieves up to 11.4× (5.3× on average) better performance than private cache bypassing for the SPLASH-3 benchmarks.

International audience

Architecture Analysis and Design Language (AADL) is a standard in avionics system design. However, the communication patterns provided by AADL are not sufficient to the current context of Real-Time Embedded System (RTES) in which some multi-periodic communication patterns may occur. We propose an extension of a precedence model between tasks of different periods (multiperiodic communication). This relies on the Semaphore Precedence Constraint (SPC) model that is inspired from the concept of Semaphore, and more specifically on the m-n producer/consumer paradigm. We reinforce the SPC semantics by allowing cycles in the SPC precedence graph. We also present another viewpoint on the periodicity of tasks system using SPC based on a graph apart from the encoding technique presented in the SPC seminal work. An implementation of SPC in AADL and its associated analysis tool are also provided to study the temporal behaviour of systems using SPC.

Control-command systems must usually satisfy a set of high-level end-to-end timing constraints to ensure their correctness. We propose a formal approach to verify these properties directly at the model level. First, we introduce a small language for specifying arbitrary end-to-end constraints. Then, we show how to verify any constraint of this language for a system represented with a multi-periodic synchronous model, a model that retains the main concepts of data-flow oriented programming languages (such as Matlab/Simulink, synchronous languages or AADL). One advantage of this approach is that it is simpler to verify end-to-end constraints at the model level, early in the development process, rather than at the implementation level.

Many-core processors offer massively parallel computation power representing a good opportunity for the design of highly integrated avionics systems. Such designs must face several challenges among which 1) temporal isolation must be ensured between applications and 2) bounds of WCET must be computed for real-time safety critical applications. In order to partially address those issues, we propose an appropriate execution model, that restricts the applications behaviours, which has been implemented on the Kalray MPPA-256. We tested the correctness of the approach through a series of benchmarks and the implementation of a case study.

Although multi/many-core platforms enable the parallel execution of tasks, the sharing of resources may lead to long WCETs that fail to meet the real-time constraints of the system. Then, a safe solution is the execution of the most critical tasks in isolation followed by the execution of the remaining tasks. To improve the system performance, we propose an approach where a critical task can run in parallel with less critical tasks, as long as the real-time constraints are met. When no further interferences can be tolerated, the proposed run-time control suspends the low critical tasks until the termination of the critical task. In this paper, we describe the design and prove the correctness of our approach. To do so, a graph grammar is defined to formally model the critical task as a set of control flow graphs on which a safe partial WCET analysis is applied and used at run-time to control the safe execution of the critical task.

This paper presents a complete case study - named ROSACE for Research Open-Source Avionics and Control Engineering - that goes from a baseline flight controller, developed in MATLAB/SIMULINK, to a multi-periodic controller executing on a multi/many-core target. The interactions between control and computer engineers are highlighted during the development steps, in particular by investigating several multi-periodic configurations. We deduced ways to improve the discussion between engineers in order to ease the integration on the target. The whole case study is made available to the community under an open-source license.

This work describes a framework for distributed simulation of cyber-physical systems (CPS). Modern CPS comprise large numbers of heterogeneous components, typically designed in very different tools and languages that are not or not easily compose able. Evaluating such large systems requires tools that integrate all components in a systematic, well-defined manner. This work leverages existing frameworks to facilitate the integration offers validation by simulation. A framework for distributed simulation is the IEEE High-Level Architecture (HLA) compliant tool CERTI, which provides the infrastructure for co-simulation of models in various simulation environments as well as hardware components. We use CERTI in combination with Ptolemy II, an environment for modeling and simulating heterogeneous systems. In particular, we focus on models of a CPS, including the physical dynamics of a plant, the software that controls the plant, and the network that enables the communication between controllers. We describe the Ptolemy extensions for the interaction with HLA and demonstrate the approach on a flight control system simulation.

This paper describes an end-to-end framework for the design and the implementation of real-time systems on a many-core architecture. The system, described in the multi-rate synchronous language Prelude, is translated into a set of communicating periodic tasks. We present a first heuristic to compute a partitioning of this task set that takes into account the specifics of the underlying platform, the Intel Single-chip Cloud Computer (SCC). In particular, the heuristic considers the communication between tasks. Furthermore, we provide a schedulability analysis that is used to validate the partitioning. We successfully apply the heuristic to several realistic use cases to evaluate the effectiveness of the proposed framework. For executing the task set, we have developed a run-time environment based on a bare-metal library that allows partitioned non-preemptive earliest deadline first (EDF) scheduling and manages the communication between tasks via the message passing mechanisms provided by the Intel SCC. The evaluation shows that the run-time overheads introduced by the framework are reasonably low.

The software architecture of a critical embedded control system generally consists of a set of multi-periodic communicating tasks. In order to be able to describe such a system, we define the notion of semaphore precedence constraint, which supports multi-rate communications that follow regular repetitive patterns. We propose a feasibility test for EDF and we study three implementations, for periodic task sets related by such extended precedences on monoprocessor architectures.

The Integrated Modular Avionics (IMA) architectures have been defined for sharing communication and computation resources. The aim of this paper is to evaluate latency and freshness properties of functions implemented on IMA platforms. The two contributions are : (1) a modeling approach for IMA platforms based on the tagged signal model and the abstraction of the network, (2) the definition of an evaluation method for these properties based on Integer Linear Programming (ILP). The industrial applicability of the method is showed on an Airbus A380-like platform. We propose a discussion on the significance of the over-approximations induced by the abstraction. This work is supported by the French National Research Agency within the Satrimmap project.

This article studies the scheduling of critical embedded systems, which consist of a set of communicating periodic tasks with constrained deadlines. Currently, tasks are usually sequenced manually, partly because available scheduling policies do not ensure the determinism of task communications. Ensuring this determinism requires scheduling policies supporting task precedence constraints (which we call dependent tasks), which are used to force the order in which communicating tasks execute. We propose fixed priority scheduling policies for different classes of dependent tasks: with simultaneous or arbitrary release times, with simple precedences (between tasks of the same period) or extended precedences (between tasks of different periods). We only consider policies that do not require synchronization mechanisms (like semaphores). This completely prevents deadlocks or scheduling anomalies without requiring further proofs.

The design of high-performance stream-processing systems is a fast growing domain, driven by markets such like high-end TV, gaming, 3D animation and medical imaging. It is also a surprisingly demanding task, with respect to the algorithmic and conceptual simplicity of streaming applications. It needs the close cooperation between numerical analysts, parallel programming experts, real-time control experts and computer architects, and incurs a very high level of quality insurance and optimization.In search for improved productivity, we propose a programming model and language dedicated to high-performance stream processing. This language builds on the synchronous programming model and on domain knowledge -- the periodic evolution of streams -- to allow correct-by-construction properties to be proven by the compiler. These properties include resource requirements and delays between input and output streams. Automating this task avoids tedious and error-prone engineering, due to the combinatorics of the composition of filters with multiple data rates and formats. Correctness of the implementation is also difficult to assess with traditional (asynchronous, simulation-based) approaches. This language is thus provided with a relaxed notion of synchronous composition, called n-synchrony: two processes are n-synchronous if they can communicate in the ordinary (0-)synchronous model with a FIFO buffer of size n.Technically, we extend a core synchronous data-flow language with a notion of periodic clocks, and design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed or correlated. This relaxation is associated with two sub-typing rules in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic transformation into a standard synchronous program. We formally define the semantics of the language and prove the soundness and completeness of its clock calculus and synchronization transformation. Finally, the language is compared with existing formalisms.

We propose a programming model dedicated to real-time video-streaming applications for embedded media devices, including high-definition TVs. This model is built on the synchronous programming model extended with domain-specific knowledge --- periodic evolution of streams --- to allow correct-by-construction properties of the application to be proven by the compiler. These properties include buffer requirements and delays between input and output streams.Such properties are tedious to analyze by hand, due to the combinatorics of video filters, multiple data rates and formats. We show how to extend a core synchronous data-flow language with a notion of periodic clocks, and to design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed. This relaxation is associated with a subtyping rule in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic program transformation.