We present here the main features and lessons learned from the first edition of what has now become the ECRTS industrial challenge, together with the final description of the challenge and a comparative overview of the proposed solutions. This verification challenge, proposed by Thales, was first discussed in 2014 as part of a dedicated workshop (FMTV, a satellite event of the FM 2014 conference), and solutions were discussed for the first time at the WATERS 2015 workshop. The use case for the verification challenge is an aerial video tracking system. A specificity of this system lies in the fact that periods are constant but known with a limited precision only. The first part of the challenge focuses on the video frame processing system. It consists in computing maximum values of the end-to-end latency of the frames sent by the camera to the display, for two different buffer sizes, and then the minimum duration between two consecutive frame losses. The second challenge is about computing end-to-end latencies on the tracking and camera control for two different values of jitter. Solutions based on five different tools - Fiacre/Tina, CPAL (simulation and analysis), IMITATOR, UPPAAL and MAST - were submitted for discussion at WATERS 2015. While none of these solutions provided a full answer to the challenge, a combination of several of them did allow to draw some conclusions.

Logical Execution Time (LET) is a timed programming abstraction, which features predictable and composable timing. It has recently gained considerable attention in the automotive industry, where it was successfully applied to master the distribution of software applications on multi-core electronic control units. However, the LET abstraction in its conventional form is only valid within the scope of a single component. With the recent introduction of System-level Logical Execution Time (SL LET), the concept could be transferred to a system-wide scope. This article improves over a first paper on SL LET, by providing matured definitions and an extensive discussion of the concept. It also features a comprehensive evaluation exploring the impacts of SL LET with regard to design, verification, performance, and implementability. The evaluation goes far beyond the contexts in which LET was originally applied. Indeed, SL LET allows us to address many open challenges in the design and verification of complex embedded hardware/software systems addressing predictability, synchronization, composability, and extensibility. Furthermore, we investigate performance trade-offs, and we quantify implementation costs by providing an analysis of the additionally required buffers.

The current trend in modeling and analyzing real-time systems is toward tighter yet safe timing constraints. Many practical real-time systems can de facto sustain a bounded number of deadline-misses, i.e., they have Weakly-Hard Real-Time (WHRT) constraints rather than hard real-time constraints. Therefore, we strive to provide tight Deadline Miss Models (DMMs) in complement to tight response time bounds for such systems. In this work, we bound the distribution of deadline-misses for task sets running on uniprocessors using the Earliest Deadline First (EDF) scheduling policy. We assume tasks miss their deadlines due to transient overload resulting from sporadic jobs, e.g., interrupt service routines. We use Typical Worst-Case Analysis (TWCA) to tackle the problem in this context. Also, we address the sources of pessimism in computing DMMs, and we discuss the limitations of the proposed analysis. This work is motivated by and validated on a realistic case study inspired by industrial practice (satellite on-board software) and on a set of synthetic test cases. The synthetic experiment is dedicated to extensively study the impact of EDF on DMMs by presenting a comparison between DMMs computed under EDF and Rate Monotonic (RM). The results show the usefulness of this approach for temporarily overloaded systems when EDF scheduling is considered. They also show that EDF is especially useful for WHRT tasks.

This paper introduces CertiCAN, a tool produced using the Coq proof assistant for the formal certification of CAN analysis results. Result certification is a process that is light-weight and flexible compared to tool certification, which makes it a practical choice for industrial purposes. The analysis underlying CertiCAN, which is based on a combined use of two well-known CAN analysis techniques, is computationally efficient. Experiments demonstrate that CertiCAN is faster than the corresponding certified combined analysis. More importantly, it is able to certify the results of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. This result paves the way for a broader acceptance of formal tools for the certification of real-time systems analysis results.

In this paper, we introduce the first verification method which is able to provide weakly-hard real-time guarantees for tasks and task chains in systems with multiple resources under partitioned scheduling with fixed priorities. Existing weakly-hard real-time verification techniques are restricted today to systems with a single resource. A weakly-hard real-time guarantee specifies an upper bound on the maximum number m of deadline misses of a task in a sequence of k consecutive executions. Such a guarantee is useful if a task can experience a bounded number of deadline misses without impacting the system mission. We present our verification method in the context of switched networks with traffic streams between nodes, and demonstrate its practical applicability in an automotive case study.

This paper presents a generic proof of Typical Worst-Case Analysis (TWCA), an analysis technique for weakly-hard real-time uniprocessor systems. TWCA was originally introduced for systems with fixed priority preemptive (FPP) schedulers and has since been extended to fixed-priority nonpreemptive (FPNP) and earliest-deadline-first (EDF) schedulers. Our generic analysis is based on an abstract model that characterizes the exact properties needed to make TWCA applicable to any system model. Our results are formalized and checked using the Coq proof assistant along with the Prosa schedulability analysis library. Our experience with formalizing real-time systems analyses shows that this is not only a way to increase confidence in our claimed results: The discipline required to obtain machine checked proofs helps understanding the exact assumptions required by a given analysis, its key intermediate steps and how this analysis can be generalized.

One major issue that hinders the use of performance analysis in industrial design processes is the pessimism inherent to any analysis technique that applies to realistic system models. Indeed, such analyses may conservatively declare unschedulable systems that will in fact never miss any deadlines. We advocate the need to compute not only tight upper bounds on worst-case behaviors but also tight lower bounds. As a first step, we focus on uniprocessor systems executing a set of sporadic or periodic hard real-time task chains. Each task has its own priority, and the chains are scheduled according to the fixed-priority pre-emptive scheduling policy. Computing the worst-case end-to-end latency (WCEL) of each chain is complex because of the intricate relationship between the task priorities. Compared to the state of the art, our analysis provides upper bounds on the WCEL in the more general case of asynchronous task chains, and also provides lower bounds on the WCEL both for synchronous and asynchronous chains. Our computed lower bounds correspond to actual system executions exhibiting a behavior that is as close to the worst case as possible, while all other approaches rely on simulations. Extensive experiments show the relevance of lower bounds on the worst-case behavior for the industrial design of real-time embedded systems.

Real-time systems with functional dependencies between tasks often require end-to-end (as opposed to task-level) guarantees. For many of these systems, it is even possible to accept the possibility of longer end-to-end delays if one can bound their frequency. Such systems are called weakly-hard. In this paper we provide end-to-end deadline miss models for systems with task chains using Typical Worst-Case Analysis (TWCA). This bounds the number of potential deadline misses in a given sequence of activations of a task chain. To achieve this we exploit task chain properties which arise from the priority assignment of tasks in static-priority preemptive systems. This work is motivated by and validated on a realistic case study inspired by industrial practice and derived synthetic test cases.

In this paper, we present an extension of slack analysis for budgeting in the design of weakly-hard real-time systems. During design, it often happens that some parts of a task set are fully specified while other parameters, e.g. regarding recovery or monitoring tasks, will be available only much later. In such cases, slack analysis can help anticipate how these missing parameters can influence the behavior of the whole system so that a resource budget can be allocated to them. It is, however, sufficient in many application contexts to budget these tasks in order to preserve weakly-hard rather than hard guarantees. We thus present an extension of slack analysis for deriving task budgets for systems with hard and weakly-hard requirements. This work is motivated by and validated on a realistic case study inspired by industrial practice.

Real-time systems with functional dependencies between tasks often require guarantees on end-to-end delays. For many of these systems, end-to-end deadline misses are accepted if one can limit their frequency. Such systems are called weaklyhard. Recent work has shown that typical worst-case analysis (TWCA) can compute an upper bound on the number of potential deadline misses in a sequence of activations of a task chain. In a joint collaboration between Thales and TU Braunschweig, the use of TWCA to limit the number of deadline misses in an aerial video tracking (AVT) system was evaluated. The AVT case-study, the complete automated model-based tool chain from the design environment to the timing verification using TWCA, as well as the results of the evaluation will be presented in the demonstration. The tool chain involves four tools: the design modeling tool CAPELLA extended by a performance viewpoint which allows annotating the design model with timing properties needed to perform TWCA, the pivot model TEMPO which handles mismatches between the semantics of the design model and the semantics of the model used in TWCA, the scheduling analysis tool pyCPA that performs TWCA and finally the graphical tool TimingGraphics used to visualize the TWCA results. To show the pertinence of the use of TWCA, we will also compare in the demonstration the obtained results with those obtained using worst-case analysis and simulation.

This paper presents the first steps toward a formally proven tool for schedulability analysis of tasks with offsets. We formalize and verify the seminal response time analysis of Tindell by extending the Prosa proof library, which is based on the Coq proof assistant. Thanks to Coq's extraction capabilities, this will allow us to easily obtain a certified analyzer. Additionally, we want to build a Coq certifier that can verify the correctness of results obtained using related (but uncertified), already existing analyzers. Our objective is to investigate the advantages and drawbacks of both approaches, namely the certified analysis and the certifier. The work described in this paper as well as its continuation is intended to enrich the Prosa library.

We focus on the problem of computing tight deadline miss models for real-time systems, which bound the number of potential deadline misses in a given sequence of activations of a task. In practical applications, such guarantees are often sufficient because many systems are in fact not hard real-time. Our major contribution is a general formulation of that problem in the context of systems where some tasks occasionally experience sporadic overload. Based on this new formulation, we present an algorithm that can take into account fine-grained effects of overload at the input of different tasks when computing deadline miss bounds. Finally, we show in experiments with synthetic as well as industrial data that our algorithm produces bounds that are much tighter than in previous work, in sufficiently short time.

For some automotive applications, worst case performance guarantees are too expensive, but a minimum level of performance must be formally guaranteed. For such applications, we have developed an approach called Typical Worst Case Analysis (TWCA) which can formally bound the number of violations of the computed response-time guarantee in a given time window. In this paper, we demonstrate how it can be used to analyze a real CAN bus with complex load patterns. We investigate the effects of these load patterns and show how the necessary parameters can be derived and verified from traces and specifications. We compare the results to the commonly used base load approximation --- like a 50%-limit for cyclic load --- showing superior accuracy and expressiveness.

Weakly-hard time constraints have been proposed for applications where occasional deadline misses are permitted. Recently, a new approach called Typical Worst-Case Analysis (TWCA) has been introduced which exploits similar constraints to bound response times of systems with sporadic overload. In this paper, we extend that approach for static priority preemptive and non-preemptive scheduling to determine the maximum number of deadline misses for a given deadline. The approach is based on an optimization problem which trades off higher priority interference versus miss count. We formally derive a lattice structure for the possible combinations that lays the ground for an integer linear programming (ILP) formulation. The ILP solution is evaluated showing effectiveness of the approach and far better results than previous TWCA.

The theories underlying control engineering and real-time systems engineering use idealized models that mutually abstract from central aspects of the other discipline. Control theory usually assumes jitter-free sampling and negligible (constant) input-output latencies, disregarding complex real-world timing effects. Real-time systems theory uses abstract performance models that neglect the functional behavior and derives worst-case situations with limited expressiveness for control functions, e.g., In physically dominated automotive systems. In this paper, we propose an approach that integrates state-of-the art timing models into functional analysis. We combine physical, control and timing models by representing them as a network of hybrid automata. Closed-loop properties can then be verified on this hybrid automata network by using standard model checkers for hybrid systems. Since the computational complexity is critical for model checking, we discuss abstract models of timing behavior that seem particularly suited for this type of analysis. The approach facilitates systematic co-engineering between both control and real-time disciplines, increasing design efficiency and confidence in the system. The approach is illustrated by analyzing an industrial example, the control software of an electro-mechanical braking system, with the hybrid model checker Space Ex.

Response time analysis, which determines whether timing guarantees are satisfied for a given system, has matured to industrial practice and is able to consider even complex activation patterns modelled through arrival curves or minimum distance functions. On the other side, sensitivity analysis, which determines bounds on parameter variations under which constraints are still satisfied, is largely restricted to variation of single-valued parameters as e.g. task periods. In this paper we provide a sensitivity analysis to determine the bounds on the admissible activation pattern of a task, modelled through a minimum distance function. In an evaluation on a set of synthetic testcases we show, that the proposed algorithm provides significantly tighter bounds, than previous exact analyses, that determine allowable parametrizations of activation patterns.

In this paper we propose a new method for the analysis of response times in uni-processor real-time systems where task activation patterns may contain sporadic bursts. We use a burst model to calculate how often response times may exceed the worst-case response time bound obtained while ignoring bursts. This work is of particular interest to deal with dual-cyclic frames in the analysis of CAN buses. Our approach can handle arbitrary activation patterns and the static priority preemptive as well as non-preemptive scheduling policies. Experiments show the applicability and the benefits of the proposed method.

The advent of multi- and many-core processors comes with new challenges and opportunities for the designer of embedded real-time applications. By using parallel programming techniques (e.g. OpenMP) software engineers can leverage from the available hardware parallelism and speed up the algorithms. The inherent redundancy of multi-core architectures can also be used to implement fault-tolerance by executing code redundantly on multiple cores in parallel. Parallel programming and redundant execution are typical examples for fork-join tasks in which the program is partially parallelized. However, complex synchronization of parallel segments across multiple cores can cause unanticipated effects. This is especially problematic in hard real-time applications where data must be available in bounded time (e.g. stereo vision for pedestrian detection). The contribution of this work is a novel worst-case response time analysis which accounts for synchronization of fork-join tasks with arbitrary deadlines. We apply the analysis to the Romain framework which extends the L4 micro kernel by redundant multithreading targeted towards fault-tolerant embedded systems. By using formal analysis, we show that parallelizing workloads can lead to drastic performance impairments compared to traditional sequential execution if not done carefully.

Modeling and analysis of timing information are essential to the design of real-time systems. In this domain, research related to probabilistic analysis is motivated by the desire to refine results obtained using worst-case analysis for systems in which the worst-case scenario is not the only relevant one, such as soft real-time systems. This paper presents an overview of the existing solutions for probabilistic timing analysis, focusing on challenges they have to face. We discuss in particular two new trends toward Probabilistic Real-Time Calculus and Typical-Case Analysis which rise to some of these challenges.

This paper presents a new compositional approach providing safe quantitative information about real-time systems. Our method is based on a new model to describe sporadic overload at the input of a system. We show how to derive from such a model safe quantitative information about the response time of each task. Experiments demonstrate the efficiency of this approach on a real-life example. In addition we improve the state of the art in compositional performance analysis by introducing execution time models which take into account several consecutive executions and by using tighter bounds for computing output event models.

Model-based verification of timing properties has become industrial practice in design processes of safety-critical hard real-time systems. To validate the correctness of the used verification model, systems are additionally monitored during regular operation. With a growing variety of activation patterns considered in verification, some of them with infinite range capturing arbitrary activation patterns, the known approaches to monitoring, which assume periodic streams, have become inapplicable or they suffer from large overhead due to piecewise continuous time monitoring. In this paper we present a light-weight monitoring approach for arbitrary activation patterns. It profits from the discrete time property of a minimum distance event representation which is used instead of the continuous time representation used in earlier approaches. The method has a configurable constant runtime overhead in terms of memory and computation and allows conservative monitoring of a given arbitrary minimum distance function. Furthermore, we provide conditions under which the monitoring function is exact.

In this paper, we add to the usual notion of contract a structural part specifying the composition operator used to compose the component and its environment. We provide a framework for compositional verification including a proof rule for dominance between contracts based on apparent circular reasoning. We also briefly describe a consistency condition and a method based on assumption generation to generate or refine contracts.