Development of a Schedulability Analysis Framework Based on pTPN and UPPAAL with Stopwatches

This paper proposes an original schedulability framework which is based on preemptive Time Petri Nets (pTPNs) and UPPAAL with stopwatches (UPPAALSW). The realization enables a real-time tasking set, along with precedence constraints in the form of data control, message passing etc., to be uniformly formalized using pTPNs and then analyzed through model checking using UPPAALSW in the presence of a reusable library of template processes modelling transitions of the source pTPNs specification and the scheduler algorithm which can be based on fixed priority or earliest deadline first. The paper first introduces and motivates the proposed approach by relating it to similar work described in literature, then summarizes the pTPNs formalism through a modelling example. After that the prototyped library in UPPAALSW is presented and put to work for model checking the chosen real-time tasking set. Analysis of models which depend e.g. on non deterministic execution times and sporadic arrival times of tasks, is conditioned by the use of an over approximation in the generation of the model state graph.