TY - GEN
T1 - Simulation-based verification of hybrid automata stochastic logic formulas for stochastic symmetric nets
AU - Amparore, Elvio Gilberto
AU - Barbot, Benoît
AU - Beccuti, Marco
AU - Donatelli, Susanna
AU - Franceschinis, Giuliana
PY - 2013
Y1 - 2013
N2 - The Hybrid Automata Stochastic Logic (HASL) has been recently defined as a flexible way to express classical performance measures as well as more complex, path-based ones (generically called "HASL formulas"). The considered paths are executions of Generalized Stochastic Petri Nets (GSPN), which are an extension of the basic Petri net formalism to define discrete event stochastic processes. The computation of the HASL formulas for a GSPN model is demanded to the COSMOS tool, that applies simulation techniques to the formula computation. Stochastic Symmetric Nets (SSN) are a high level Petri net formalism, of the colored type, in which tokens can have an identity, and it is well known that colored Petri nets allow one to describe systems in a more compact and parametric form than basic (uncolored) Petri nets. In this paper we propose to extend HASL and COSMOS to support colors, so that performance formulas for SSN can be easily defined and evaluated. This requires a new definition of the logic, to ensure that colors are taken into account in a correct and useful manner, and a significant extension of the COSMOS tool.
AB - The Hybrid Automata Stochastic Logic (HASL) has been recently defined as a flexible way to express classical performance measures as well as more complex, path-based ones (generically called "HASL formulas"). The considered paths are executions of Generalized Stochastic Petri Nets (GSPN), which are an extension of the basic Petri net formalism to define discrete event stochastic processes. The computation of the HASL formulas for a GSPN model is demanded to the COSMOS tool, that applies simulation techniques to the formula computation. Stochastic Symmetric Nets (SSN) are a high level Petri net formalism, of the colored type, in which tokens can have an identity, and it is well known that colored Petri nets allow one to describe systems in a more compact and parametric form than basic (uncolored) Petri nets. In this paper we propose to extend HASL and COSMOS to support colors, so that performance formulas for SSN can be easily defined and evaluated. This requires a new definition of the logic, to ensure that colors are taken into account in a correct and useful manner, and a significant extension of the COSMOS tool.
KW - generalized stochastic petri nets
KW - hybrid automata stochastic logic
KW - simulation-based verification
KW - stochastic symmetric nets
UR - http://www.scopus.com/inward/record.url?scp=84878626643&partnerID=8YFLogxK
U2 - 10.1145/2486092.2486124
DO - 10.1145/2486092.2486124
M3 - Conference contribution
AN - SCOPUS:84878626643
SN - 9781450319201
T3 - SIGSIM-PADS 2013 - Proceedings of the 2013 ACM SIGSIM Principles of Advanced Discrete Simulation
SP - 253
EP - 264
BT - SIGSIM-PADS 2013 - Proceedings of the 2013 ACM SIGSIM Principles of Advanced Discrete Simulation
T2 - 2013 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, SIGSIM-PADS 2013
Y2 - 19 May 2013 through 22 May 2013
ER -