The quality of timing guarantees ensured through worst-case-execution time analysis and schedulability tests - required to be both sound and precise - is directly influenced by the predictability properties of the execution platform. A platform is considered predictable when safe and precise bounds can be computed through analysis tools. Counter-intuitive and Amplification Timing Anomalies (TAs) are detrimental to predictability and thus may make it much harder/impossible to compute such bounds. In order to address this issue, research has followed two orthogonal approaches, (i) designing predictable execution platforms and (ii) characterizing counter-intuitive TAs through formal definitions. However, predictable designs rarely apply any formal definitions of timing anomalies. This paper aims at investigating precisely this relationship. We first show how a previously proposed definition of counter-intuitive TAs can be applied to the predictable in-order processor SIC. We then extend this approach in order to provide the first formal definition of both counterintuitive and amplification effects. The proposed definitions are then evaluated on a regular in-order processor as well as the predictable SIC core using a systematic approach that allows to assess their applicability and relevance. Finally, we prove, for the first time, the absence of some, but not all, TA effects in SIC

Static worst-case timing analyses compute safe timing bounds of applications running in real-time systems. These bounds are necessary to evaluate the strict timing constraints of real-time systems. Moreover, the inherent complexity of such systems demands that their timing analyses are able to cope with the large resulting state space. In this direction, a potential solution is to perform compositional timing analysis, where the system-level timing is obtained from component-level timings. Undesired timing phenomena, called timing anomalies, threaten the soundness of (compositional) timing analyses. In this work, we investigate how the industrial superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. Firstly, we adapt and extend a specialized abstraction, called canonical pipeline model, to capture the amplification effects in a formal model of the TriCore architecture. Then, we use model checking to efficiently detect amplification timing anomalies and report the associated complexity results. Finally, we aim for better precision as we design and implement counterexample-based methods so as to uncover patterns leading to such anomalies.

Intuitively, a counter-intuitive timing anomaly manifests when a locally faster execution becomes globally slower. While the presence of such timing anomalies threatens the soundness and/or scalability of timing analyses, tools to systematically detect them do not exist. The main reason lies in the absence of a definition of counter-intuitive timing anomalies that establishes relations between local and global timing effects. In this paper, we address these relations through an important concept, that of causality, which we further use to revise the formalization of counter-intuitive timing anomalies. We also propose a specialized instance of the notions to implement a detection procedure for out-of-order pipelines.

Définitions et procédures de détection des anomalies temporelles pour la vérification formelle de la prédictibilité des systèmes temps-réel Les systèmes temps-réel sont souvent validés par des analyses temporelles, qui sont mises en péril par des anomalies temporelles (AT). Une AT contre-intuitive a lieu quand une accélération locale conduit à un ralentissement global, et une AT d'amplification, quand un ralentissement local entraîne un ralentissement encore plus grand.Alors que les AT contre-intuitives menacent le bien-fondé ou la flexibilité des analyses, il n'existe pas d'outils pour les détecter de manière systématique. Nous proposons une structure formelle unifiée pour évaluer les définitions des AT, concluant au manque d'une définition pratique, principalement dû à l'absence de relations entre les effets temporels locaux et globaux. Nous y répondons par la causalité, que nous utilisons pour revoir la formalisation de ces AT. Nous proposons aussi une instance des notions spécialisée pour les pipelines out-of-order. Nous évaluons notre procédure de détection subséquente sur des exemples illustratifs et bancs de tests, montrant qu'elle permet de capturer précisément les AT.La complexité des systèmes exige que leurs analyses gèrent l'important espace d'états résultant. Une solution est de réaliser des analyses compositionnelles, précisément menacées par les AT d'amplification. Nous faisons progresser leur étude en montrant comment une abstraction spécialisée peut être adaptée pour un processeur industriel, en modélisant les caractéristiques temporelles clés avec des réductions appropriées. Nous illustrons aussi à partir de cette classe d'AT comment des stratégies de vérification peuvent être utilisées en vue de l'obtention de motifs d'AT.

Correctness is an important concern during the development of real-time systems. In addition to the functional correctness, the timing behavior is often formally verified in order to ensure that correct results are delivered in-time for all possible execution conditions. The timing behavior of real-time software is thus often validated through a rigorous timing analysis that aims at determining the worst-case execution time.Timing anomalies present a major obstacle during the validation of timing properties on modern computer platforms. Out-of-order execution and concurrent accesses to shared resources may sometimes lead to – at first sight – surprising timing behavior. Several (semi-)formal definitions have been proposed in the literature in order to capture such situations. However, as we present in this work, none of the existing definitions appears to be precise enough to be systematically used for detecting timing anomalies in modern processors with out-of-order execution.

Real-time systems are subject to strong timing requirements, and thus rely on worst-case timing analyses to safely address them. Undesired timing phenomena, called timing anomalies, threaten the soundness of timing analyses. In this regard, we consider the following inauspicious partnership - a compositional timing analysis and amplification timing anomalies. Precisely, we investigate how the industrial, superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. We adapt and extend a specialized abstraction, called canonical pipeline model, to quantify the amplification effects in a model of a dual-pipelined TriCore, its asynchronous store buffer, data dependencies, and structural hazards. We use model checking to efficiently detect amplification timing anomalies and report the associated complexity results.

Driverless systems are currently used in a variety of applications such as self-driving cars, automated transportation systems at harbors, factories and hospitals. However, only a few applications are actually designed to work in a shared environment with humans because such a system would require an autonomous system instead of automated vehicles. In the project Autonomous Fleet, we consider a system-of-system problem where the coordination and navigation of a fleet of autonomous vehicles for dynamic environments with people is required. On the one hand, the coordination system considers the whole fleet, i.e., the position and goal of each vehicle. Its duty is to propose a routing solution for all vehicles by setting checkpoints. This poses similarities with the traffic control system for vehicle drivers on roads - it affects the driving behavior but cannot control it. On the other hand, each vehicle has its own navigation system which is responsible for how to drive between checkpoints and avoid collisions with (dynamic) obstacles and is therefore autonomous. The focus of this work is on the coordination system with algorithms for collision-free routing for a fleet of autonomous vehicles.

Autonomous vehicles are, in contrast to classical automated guided vehicles (AGVs), less predictable in their behavior and drive time. Therefore, the issue of how to efficiently control these vehicles arises, because autonomous agents need to be coordinated and not controlled, to give autonomous behaviors and actions space. The scientific contribution of this paper is a novel approach, based on prioritized planning to target this issue as well as an open source framework for evaluation and comparison. Prioritized planning has the disadvantage of being neither optimal nor complete, however, it has the advantage of being computationally feasible. This work utilizes prioritized planning to significantly increase the set of feasible scenarios through collision prevention: by locally finding alternative routes and adding them to the search graph. The paper clearly formulates the extensions needed and delineates the approach’s limits, as it is neither optimal nor complete. More importantly, however, our method calculates routes for each vehicle with inter-vehicle synchronization, enabling vehicles to execute the plan in a distributed fashion without centralized control, thereby allowing autonomous behavior. Finally, results are verified by comparing our Multi Robot Router (MRR) proposed in this work to classical approaches. The software developed as well as the test sets are publicly available for ROS and the simulation environment.

This work presents a tracking and control mechanism for an UGV (Unmanned Ground Vehicle) and its integration into ROS (Robot Operating System). The overall goal of which this work is part, is the creation of a fleet of ackermann robots to conduct studies in the field of autonomous driving. In order to achieve this goal a 1:10 RC-race car model is equipped with an Arduino board to control the vehicles actuators and a Raspberry Pi to host the ROS server. In addition, a physics simulation is used to model this car for testing. The shown results support the used velocity motion model and the applicability of the developed interface to control both platforms.