Qualitative and quantitative model checking of distributed probabilistic timed actors

This article proposes an approach to modelling and analysis of distributed probabilistic timed actors. The approach rests on a lightweight infrastructure of actors -Theatre- whose design aims to favoring the development of predictable time-dependent applications. Adopted actors are thread-less and their evolution is transparently regulated by a customizable control layer which has a reflective link with the application. A Theatre system consists of a collection of interacting computing nodes (theatres) each one hosting a sub system of local actors. The control layers of the various theatre components coordinate each other so as to enforce a common global time notion (real or simulated time). The abstract Theatre modelling language can be reduced in a case to Uppaal, which opens to the analysis of the functional/non-functional aspects of a distributed system. A key factor of the reduction process concerns the possibility of making both a non-deterministic analysis of an actor model (checking that something, e.g., an event, can occur), and a quantitative evaluation of system behavior by statistical model checking of the same model (e.g., estimating the probability for an event to occur). The paper describes the Theatre architecture and introduces a real-time case study which is used as a running example throughout the paper. The operational semantics of Theatre is provided and the proposed reduction of Theatre actors on top of Uppaal detailed through the chosen example. Some experimental results are reported about qualitative and quantitative analysis of the case study. Finally, conclusions are presented with an indication of further work.