Modelling and Analysis of Partially Stochastic Time Petri Nets Using Uppaal Model Checkers

Modelling and analysis of time-dependent concurrent/distributed systems is very challenging when such systems also exhibit a stochastic behavior. In this paper, the partially stochastic Time Petri Net formalism (psTPN) is introduced, which has the expressive power to model realistic complex systems. Each transition owns both a non-deterministic temporal interval and a stochastic duration established by a generally distributed (i.e., not necessarily Markovian) probabilistic function whose samples are constrained to occur in the associated time interval. A psTPN model admits two possible interpretations: the non-deterministic (which ignores stochastic aspects), useful for qualitative analysis (establishing that an event can possibly occur) and the stochastic one (which considers stochastic behavior), useful for quantitative analysis (estimating the probability for an event to actually occur). The paper focuses on the reduction of psTPN onto Uppaal timed automata which permit non-deterministic analysis through the symbolic exhaustive model checker, and quantitative analysis through the statistical model checker (SMC) which rests on simulations and statistical inference. Although potentially less accurate of analysis techniques based on numerical methods and stochastic state space enumeration, this paper claims that statistical model checking can provide quantitative property assessment which is of practical engineering value. As an example, psTPN is exploited in the paper to model and evaluate a stochastic version of the Fisher timed-based mutual exclusion algorithm.