A methodology for the construction of scheduled systems

We study a methodology for constructing scheduled systems by restricting successively the behavior of the processes to be scheduled. Restriction is used to guarantee the satisfaction of two types of constraints: schedulability con-straints guaranteeing that timing properties of the processes are satised, and constraints characterizing particular scheduling algorithms including process priorities, non-idling, and preemption. The methodology is based on a controller synthesis paradigm. The main re-sults deal with the characterization of scheduling policies as safety constraints and the simplication of the synthesis process by applying a composability principle.