Abstract

The theory of supervisory control of discrete-event systems has been applied to real-time systems. The contribution of our proposed work lies in the development of a formal constructive method for controlling the preemptive execution of real-time tasks on both uniprocessor and multiprocessor systems. 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. This approach allows a unified view of scheduling theory based on the timing analysis of models of real-time applications, meaning that the problem of determining schedulability and finding out a suitable scheduling algorithm are assumed to be intermingled issues, with the solution of one in turn is a solution to the other too. First, a framework for designing universal schedulers for real-time tasks on uniprocessors based on Supervisory Control Theory (SCT) is presented. For this purpose, priorities are introduced in SCT and applied to the setting of discrete timed automata in order to develop a formal and unified framework for task scheduling on a single CPU. A universal scheduler nondeterministically selects a task for execution in such a way that all timing constraints are met in a minimally restrictive fashion, while it contains all feasible deterministic scheduling policies. We then extend that framework by providing a formal constructive method for controlling the preemptive and migrative execution of hard real-time tasks while scheduling them on a set of uniform processors. The methodology relies on the idea that the model of the scheduled system can be obtained by successive and appropriate restrictions of controllable actions of a model representing the real-time application. In uniform multiprocessors, each processor is characterized by its own computing capacity, with the interpretation that a task that executes on a processor of computing capacity s for x time units completes s x units of execution. Since we represented explicitly discrete time in our scheduler design, model sizes were considerably large. The complexity in the synthesis of a scheduler using supervisory control [62] stems from the fact that, with the synchronous product, the number of states of a composite Timed Discrete-Event System (TDES) increases exponentially with the number of real-time tasks. We have attempted to alleviate some of the state explosion problems we had faced while designing schedulers for real-time systems using supervisory control of discrete-event systems framework [39, 41], by providing an informal procedure to design schedulers with reduced state space.