Statistical Model Checking of GSPN Models
Franco Cicirelli, Christian Nigro, Libero Nigro · 2015
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.