Statistical Model Checking of GSPN Models

Franco Cicirelli, Christian Nigro, Libero Nigro

2015

Abstract

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.

Paper Citation

in Harvard Style

Cicirelli F., Nigro C. and Nigro L. (2015). Statistical Model Checking of GSPN Models . In Proceedings of the 5th International Conference on Simulation and Modeling Methodologies, Technologies and Applications - Volume 1: SIMULTECH, ISBN 978-989-758-120-5, pages 69-76. DOI: 10.5220/0005506700690076

in Bibtex Style

@conference{simultech15,
author={Franco Cicirelli and Christian Nigro and Libero Nigro},
title={Statistical Model Checking of GSPN Models},
booktitle={Proceedings of the 5th International Conference on Simulation and Modeling Methodologies, Technologies and Applications - Volume 1: SIMULTECH,},
year={2015},
pages={69-76},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005506700690076},
isbn={978-989-758-120-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 5th International Conference on Simulation and Modeling Methodologies, Technologies and Applications - Volume 1: SIMULTECH,
TI - Statistical Model Checking of GSPN Models
SN - 978-989-758-120-5
AU - Cicirelli F.
AU - Nigro C.
AU - Nigro L.
PY - 2015
SP - 69
EP - 76
DO - 10.5220/0005506700690076