Sirio: A Framework for Simulation and Symbolic State Space Analysis of non-Markovian Models

Sirio is a framework for simulation and symbolic analysis of preemptive and stochastic extensions of Time Petri Nets (TPNs), enabling an integrated approach to correctness verification and quantitative evaluation of timed concurrent systems. In particular, it supports evaluation of transient and steady-state reward measures, both through simulation and analysis. As a characterizing trait, Sirio manages models with multiple concurrently enabled generally distributed (GEN) timers that underlie a Generalized Semi-Markov Process (GSMP). We describe here the SW architecture of the framework, highlighting design choices oriented towards reusability and extensibility, and we illustrate its application to a case study in the area of quantitative evaluation.