Expressing and computing passage time measures of GSPN models with HASL

Abstract. Passage time measures specification and computation for Generalized Stochastic Petri Net models have been faced in the literature from different points of view. In particular three aspects have been developed: (1) how to select a spe-cific token (called the tagged token) and measure the distribution of the time employed from an entry to an exit point in a subnet; (2) how to specify in a flexible way any condition on the paths of interest to be measured, (3) how to efficiently compute the required distribution. In this paper we focus on the speci-fication and computation of complex passage time measures in (Tagged) GSPNs using the Hybrid Automata Stochastic Logic (HASL) and the statistical model checker COSMOS. By considering GSPN models of two different systems, no-tably, a flexible manufacturing system and a workflow, we identify a number of relevant performance measures (mainly passage-time distributions), formally ex-press them in HASL terms and assess them by means of the COSMOS tool. The interest from the measures specification point of view is provided by the possi-bility of setting one or more timers along the paths, and setting the conditions for the paths selection, based on the measured values of such timers. With respect to other specification languages allowing to use timers in the specification of per-formance measures, HASL provides timers suspension, reactivation, rate change along a path