Partial-Order Reduction for Schedule-Abstraction-based Response-Time Analyses of Non-Preemptive Tasks

The temporal correctness of safety-critical systems is typically guaranteed via a response-time analysis (RTA). However, as systems become complex (e.g., parallel tasks running on a multicore platform), most existing RTAs either become pessimistic or do not scale well. To make a trade-off between accuracy and scalability, recently, a new reachability-based RTA, called schedule-abstraction graph (SAG), has been proposed. The analysis is at least three orders of magnitude faster than other exact RTAs based on UPPAAL.One fundamental limitation of the SAG analysis is that it suffers from state-space explosion when there are large uncertainties in the timing parameters of the input jobs, which may impede its applicability to some industrial use cases. In this paper, we improve the scalability of the SAG analysis by introducing partial-order reduction (POR) rules that avoid combinatorial exploration of all possible scheduling decisions. An empirical evaluation shows that our solution is able to reduce the runtime by five orders of magnitude and the number of explored states by 98%, at a negligible cost of an over-estimation of 0.1% on the tasks' worst-case response-time (WCRT). We applied our solution on an automotive case study showing that it is able to scale to realistic systems made of hundreds of tasks for which the original analysis fails to finish.