This paper proposes a novel Petri net formalism, called stochastic preemptive time Petri nets (spTPN), for modeling and analyzing concurrent real-time systems. Stochastic preemptive time Petri nets capture resource contention, nondeterministic choice, probabilistic behavior of tasks, preemption, priorities, and periodic and sporadic tasks. The analysis technique covers verification of nonfunctional properties like jitter and end-to-end delays. The distinguishing features of the modeling formalism are: a discrete time model, maximal step semantics of concurrency, and stochastic characterization of nondeterministic and temporal choices. The proposed framework is illustrated with a simple example, and tested in a medium-size example. The framework is implemented in a tool by the authors.

The formalism is described in detail and is well illustrated with small examples. The literature on modeling and analysis of real-time systems is vast, and great care has been taken by the authors to place their work in the context of the existing work to provide a detailed comparison; hence, the paper, along with the cited works, will be of high value to researchers in this field.