We study the problem of verifying schedulability and ascertaining response time bounds of limited-preemptive parallel applications with uncertainty, scheduled on multi-core platforms. While sufficient techniques exist for analysing schedulability and response time of parallel applications under fixed-priority scheduling, their accuracy remains uncertain due to the lack of a scalable and exact analysis that can serve as a ground-truth to measure the pessimism of existing sufficient analyses. In this paper, we address this gap using formal methods. We use Timed Automata and the powerful UPPAAL verification engine to develop a generic approach to model parallel applications and provide a scalable and exact schedulability and response time analysis. This work establishes a benchmark for evaluating the accuracy of both existing and future sufficient analysis techniques. Furthermore, our solution is easily extendable to more complex task models thanks to its flexible model architecture.

Heterogeneous computing platforms running highly parallelized applications are becoming increasingly common in real-time embedded systems. This demands for expressive task models that can capture parallelism, precedence constraints and self-suspending behavior caused by work-offloading on coprocessors, access to shared resources or synchronization between tasks running on different (heterogeneous) cores. The Event-Driven Delay-induced (EDD) task model was specifically designed to address these needs. Yet, to date, a single schedulability test for the EDD task model exists, and that test is limited to the analysis of fully-preemptive partitioned scheduling.In this work, we provide the first worst-case response time analysis for limited-preemptive EDD tasks that are globally scheduled on a multicore platform. Moreover, our evaluation results show that our analysis also outperforms the state-of-the-art response time analyses for both limited-preemptive DAG tasks and self-suspending tasks.

Schedulability analyses check whether all tasks in a task set will meet their timing requirements. They thus provide a boolean answer. Some analyses may also compute bounds on the worst-case response-time (WCRT) of tasks. However, only knowing WCRT is often not enough to understand which tasks are involved in deadline-miss scenarios and under what conditions those scenarios may happen. Therefore, it is hard to infer what must be fixed to make unschedulable task sets schedulable. This issue is exacerbated when tasks are non-preemptive since they are subject to timing anomalies that are non-trivial to analyze. The schedule-abstraction technique is a relatively scalable reachability-based response-time analysis that explores the space of possible schedules to detect potential deadline misses. There-fore, it can tell which jobs (of which tasks) are involved in a deadline-miss scenario. However, the schedule abstraction framework is not yet able to provide concrete release and execution times (and therefore concrete schedules) for those jobs. The reason is that, to reduce memory consumption, the schedule abstraction framework deliberately forgets information about the job execution ordering that led to a state. It also merges states to defer state-space explosion during the state-space exploration. In this work, we propose a technique to derive concrete schedules resulting in deadline misses by augmenting the exploration phase of the schedule-abstraction technique to carry minimal extra information that allows resolving ambiguities while tracing back jobs involved in deadline-miss scenarios using our own partial-order planning algorithm.

In this paper, we propose to use Schedule Abstraction Graphs (SAGs) to determine exact worst-case latency of packets at an egress port of an Ethernet TSN switch with Time-aware Shapers (TASs). We briefly sketch how to apply the existing SAG framework in a TSN context and extend the framework with FIFO-queues and TASs.