Altisen, K.Gossler, G.Sifakis, J.2013-03-142013-03-142013-03-14200010.1007/3-540-45352-0_11https://infoscience.epfl.ch/handle/20.500.14299/90322We 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 constraints characterizing timing properties of the processes, and constraints characterizing particular scheduling algorithms including process priorities, non-idling, and preemption. The methodology is based on a controller synthesis paradigm. The main results deal with the characterization of scheduling policies as safety constraints and the simplification of the synthesis process by applying a composability principlecontrol system synthesisformal specificationgraph theoryprocessor schedulingreal-time systemsset theorytext::conference output::conference proceedings::conference paper