Statistical Model Checking of GSPN Models

Generalized Stochastic Petri Nets (GSPN) are a well-known timed extension of Petri nets suited for modelling and performance analysis of general time-dependent concurrent systems. The work described in this paper develops an original structural translation of GSPN models onto UPPAAL SMC so as to enable property estimation through statistical model checking. The actual GSPN supported formal language admits, in general, tagged tokens carrying timestamps, queuing places, normal, transport and inhibitor arcs and timed and untimed transitions. This paper describes the proposed approach and demonstrates its practical usefulness through a case study.