Work-in-Progress: Generating Counter-Examples to Schedulability Using the Schedule Abstraction.

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.