Doctoral Research (PhD)

     Research Interests:

• Supervisory Control of Timed Discrete-Event Systems

• Formalization of Real-Time Scheduling

• Real-Time Systems and Control

• Formal Methods

• Symbolic Model Checking

     Research Project:

• Real-time Scheduler Synthesis on Uniprocessor and Multiprocessor Systems In Supervisory Control of Discrete-Event Systems Framework

         The theory of supervisory control of discrete-event systems has been extended to the real-time setting. We have proposed 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, i.e., the complications of checking schedulability and determining a scheduling algorithm are considered as dual problems: a solution to the former implies a solution to the latter and vice versa. First, a framework for designing universal schedulers for real-time tasks on uniprocessors based on Supervisory Control Theory (SCT) was presented. For this purpose, priorities are introduced in SCT and applied to the setting of discrete timed automata as a control mechanism 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. The synthesis mechanism was then extended to design schedulers for hard real-time tasks upon uniform multiprocessors.