Formalizing real-time scheduling using priority-based supervisory control of discrete-event systems

In this note, we formalize real-time task scheduling by applying an extension of supervisory control theory (SCT) of discrete-event systems to real-time models. The set of all possible timed traces of the system is specified by a discrete timed automaton where each transition is associated with an event occurrence or the passage of one unit of time. We introduce priorities to SCT, and apply them to the setting of discrete timed automata in order to develop a formal and unified framework for task scheduling on a single CPU.