A modeling methodology and pre-run-time scheduling for embedded real-time software

One of the most intricate problems in the synthesis of real-time systems is the scheduling. We present a formal modeling methodology based on time Petri nets (TPN) and a framework for application-specific scheduler synthesis. Finding a feasible scheduling is not an easy task because this problem, in its general form, is NP-hard. The method proposed finds a scheduling, whether one exists, using state space exploration. The problem with this approach is the space size, which can be very large for medium to large systems. We show how to minimize this problem using behavior restrictions at system modeling, and a partial-order reduction method. Additionally, the algorithm proposed for finding a feasible schedule uses a depth-first search based method. Therefore, states are only generated if strictly necessary. It is verified through real-world experimental results that a schedule is found examining a reduced number of states.