2 octobre 2017
Étienne André (LIPN)The schedulability analysis of real-time systems (even on a single
processor) is a very difficult task, which becomes even more complex (or
undecidable) when periods or deadlines become uncertain.
In this work, we propose a unified formalism to model and formally
verify monoprocessor schedulability problems with several types of tasks
(periodic, sporadic, or more complex), most types of schedulers
(including EDF, FPS, SJF), with or without preemption, in the presence
of uncertain timing constants.
Although the general case is undecidable, we exhibit a large
decidable subclass.
We demonstrate the expressive power of our formalism on several
examples, allowing also for robust schedulability.