Schedulability Analysis for Timed Automata With Tasks

Research on modeling and analysis of real-time computing systems has been done in two areas, model checking and real-time scheduling theory. In model checking, an expressive modeling formalism such as timed automata (TA) is used to model complex systems, but the analysis is typically very expensive due to state-space explosion. In real-time scheduling theory, the analysis techniques are highly efficient, but the models are often restrictive. In this paper, we aim to exploit the possibility of applying efficient analysis techniques rooted in real-time scheduling theory to analysis of real-time task systems modeled by timed automata with tasks (TAT). More specifically, we develop efficient techniques to analyze the feasibility of TAT-based task models (i.e., whether all tasks can meet their deadlines on single-processor) using demand bound functions (DBF), a widely used workload abstraction in real-time scheduling theory. Our proposed analysis method has a pseudo-polynomial time complexity if the number of clocks used to model each task is bounded by a constant, which is much lower than the exponential complexity of the traditional model-checking based analysis approach (also assuming the number of clocks is bounded by a constant). We apply dynamic programming techniques to implement the DBF-based analysis framework, and propose state space pruning techniques to accelerate the analysis process. Experimental results show that our DBF-based method can analyze a TAT system with 50 tasks within a few minutes, which significantly outperforms the state-of-the-art TAT-based schedulability analysis tool TIMES.

Deep Learning to Predict the Feasibility of Priority-Based Ethernet Network Configurations

Machine learning has been recently applied in real-time systems to predict whether Ethernet network configurations are feasible in terms of meeting deadline constraints without executing conventional schedulability analysis. However, the existing prediction techniques require domain expertise to choose the relevant input features and do not perform consistently when topologies or traffic patterns differ significantly from the ones in the training data. To overcome these problems, we propose a Graph Neural Network (GNN) prediction model that synthesizes relevant features directly from the raw data. This deep learning model possesses the ability to exploit relations among flows, links, and queues in switched Ethernet networks and generalizes to unseen topologies and traffic patterns. We also explore the use of ensembles of GNNs and show that it enhances the robustness of the predictions. An evaluation on heterogeneous testing sets comprising realistic automotive networks shows that ensembles of 32 GNN models feature a prediction accuracy ranging from 79.3% to 90% for Ethernet networks using priorities as the Quality-of-Service mechanism. The use of ensemble models provides a speedup factor ranging from 77 to 1,715 compared to schedulability analysis, which allows a far more extensive design space exploration.

Cross-Layer Adaptation with Safety-Assured Proactive Task Job Skipping

During the operation of many real-time safety-critical systems, there are often strong needs for adapting to a dynamic environment or evolving mission objectives, e.g., increasing sampling and control frequencies of some functions to improve their performance under certain situations. However, a system's ability to adapt is often limited by tight resource constraints and rigid periodic execution requirements. In this work, we present a cross-layer approach to improve system adaptability by allowing proactive skipping of task executions, so that the resources can be either saved directly or re-allocated to other tasks for their performance improvement. Our approach includes three novel elements: (1) formal methods for deriving the feasible skipping choices of control tasks with safety guarantees at the functional layer, (2) a schedulability analysis method for assessing system feasibility at the architectural layer under allowed task job skippings, and (3) a runtime adaptation algorithm that efficiently explores job skipping choices and task priorities for meeting system adaptation requirements while ensuring system safety and timing correctness. Experiments demonstrate the effectiveness of our approach in meeting system adaptation needs.

Federated Scheduling of Sporadic DAGs on Unrelated Multiprocessors

This paper presents a federated scheduling algorithm for implicit-deadline sporadic DAGs that execute on an unrelated heterogeneous multiprocessor platform. We consider a global work-conserving scheduler to execute a single DAG exclusively on a subset of the unrelated processors. Formal schedulability analysis to find the makespan of a DAG on its dedicated subset of the processors is proposed. The problem of determining each subset of dedicated unrelated processors for each DAG such that the DAG meets its deadline (i.e., designing the federated scheduling algorithm) is tackled by proposing a novel processors-to-task assignment heuristic using a new concept called processor value . Empirical evaluation is presented to show the effectiveness of our approach.

Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.