Formal Modelling and Analysis of Probabilistic Real-Time Systems

This paper considers formal modelling and analysis of distributed timed and stochastic real-time systems. The approach is based on Stochastic Time Petri Nets (sTPN) which offer a readable yet powerful modelling language. sTPN are supported by special case tools which can ensure accuracy in the results by numerical methods and the enumeration of stochastic state classes. These techniques, though, can suffer of state explosion problems when facing large models. In this work, a reduction of sTPN onto the popular Uppaal model checkers is developed which permits both exhaustive non-deterministic analysis, which ignores stochastic aspects and it is useful for functional and temporal assessment of system behavior, and quantitative analysis through statistical model checking, useful for estimating by automated simulation runs probability measures of event occurrence. The paper provides the formal definition of sTPN and its embedding into Uppaal. A sensor network case study is used as a running example throughout the paper to demonstrate the practical applicability of the approach.