A Framework for Simulation and Symbolic State Space Analysis of Non-Markovian Models

Formal methods supporting development of safety-critical systems require tools that can be integrated within composed environments. Sirio is a framework for simulation and analysis of various timed extensions of Petri Nets, supporting correctness verification and quantitative evaluation of timed concurrent systems. As a characterizing trait, Sirio is expressly designed to support reuse and to facilitate extensions such as the definition of new reward measures, new variants of the analysis, and new models with a different semantics. We describe here the functional responsibilities and the SW architecture of the framework.