Modelling and Analysis of Distributed Asynchronous Actor Systems using Theatre

This paper introduces THEATRE, a modular software architecture whose aim is supporting modelling, analysis, design and implementation of distributed asynchronous probabilistic and timed/untimed actor systems. A key factor of THEATRE is that a same model can be transitioned without distortions from a development phase to the next one. The analysis phase is currently based on the UPPAAL Statistical Model Checker (SMC) which automatizes simulations, and uses statistical techniques (e.g., Monte Carlo-like and sequential hypothesis testing) to infer quantitative measures from the simulation runs. The design and implementation phases are based on Java. The paper describes the abstract modelling language of THEATRE and focusses on its translation to UPPAAL SMC. The approach is practically demonstrated by two modelling examples and their experimental analysis.