Parallel Simulation of Stochastic Reward Nets using Theatre

This work aims at the development of tools for supporting modelling and analysis of timed systems by Stochastic Reward Nets (SRN). In a first approach it was proposed and experimented a formal reduction of SRN over Timed Automata (TA) in the context of the Uppaal popular toolbox. The reduction has the merit to allow both exhaustive model checking of an SRN model, useful for the assessment of qualitative properties (e.g., absence of deadlocks, occurrence of particular event sequences etc.), and quantitative analysis through the statistical model checker, which is based on simulations. However, although Uppaal enabled formal reasoning on the semantics of SRN, its practical usage suffers of scalability problems, that is it can introduce severe limitations in time and space when studying complex models. To cope with this problem, this paper describes a Java implementation of the SRN operational core engine, using the lock-free and efficient Theatre actor system which permits the parallel simulation of large models. The realization can be used for functional property checking on an untimed version of a source SRN model, and quantitative estimation of measurables through simulations. The paper discusses the design and implementation of the core engine of SRN on top of Theatre, together with supported intuitive configuration process of an SRN model, and reports some experimental results using a scalable grid computing model. The experiments confirm Theatre/SRN are capable of exploiting the potential of modern multi-core machines and can deliver good execution performances on large models.