Time Petri Nets for the Schedulability Analysis of the Transactional Event

Priority-based FRP (P-FRP) is functional programming formalism for reactive systems that guaran-tees real-time response. Preempted tasks in P-FRP are aborted and have to restart when no higher prior-ity tasks are present in the execution queue. The abort and eventual restart makes the response time of a lower priority task completely dependent on the execution pattern of higher priority tasks. Exact schedulability analysis methods of P-FRP that have been presented so far require the evaluation of all release scenarios of higher priority tasks. Unfortunately, the number of such scenarios scale exponen-tially with the size of the task set making exact schedulability analysis of this execution model a com-putationally expensive proposition. The formal method of Time Petri Net (TPN) has previously been used for schedulability analysis of preemptive and non-preemptive models. TPNs for P-FRP or other transaction like execution models have not been developed yet. In this paper, we develop TPN models for the transactional execution model of P-FRP and show that TPNs offer an efficient alternative for schedulability analysis of this model. We have implemented our TPNs in the model checker ROMEO and have validated the correctness of our models through experimental task sets