Scheduling Self-Suspending Periodic Real-Time Tasks Using Model Checking

International audienceIn this paper, we address the problem of scheduling periodic, possibly self-suspending, real-time tasks. We provide schedulability tests for PFP and EDF and a feasibility test using model checking. This is done both with and without the restriction of work-conserving schedules. We also provide a method to test the sustainability w.r.t the execution and suspension durations of the schedulability and feasibility properties within a restricted interval. Finally we show how to generate an on-line scheduler for such systems when they are feasible