A symbolic schedulability technique of real-time systems modeled by P-Time Petri nets

This paper addresses the schedulability analysis of real-time systems modeled by P-Time Petri nets. The proposed approach is based on the consideration of the reachability graph of the (untimed) underlying Petri net of the studied model. The schedulability analysis is then conducted in two steps. Once a feasible firing sequence (called occurrence sequence) is highlighted, thanks to a firing instant based approach the timing constraints are added, yielding an inequality system representing its timing behavior. Thus, deciding whether a firing sequence is schedulable or not takes the form of the solution of a linear programming problem. Furthermore, the modification of a timing constraint does not alter the form of the obtained system, helping adjusting accurately timing properties in a specifications refinement purpose.