Abstract

With supervisory control, it is possible to restrict the behavior of a system by disabling a subset of controllable events. Our objective is to develop a well-established formal method for preemptive and non-preemptive task scheduling based on supervisory control. We also examine how formal methods can help address issues such as priority-based scheduling. To achieve these objectives we first introduce a model for each tasks and desired requirements. To address the priority-based scheduling we define a priority relation as a specification, which assigns a priority to each task. The task and specification models are then combined separately into a campsite model. We finally obtain a supervisory control that guaranties all desires requirements are met by using the supervisory control theory.