Actor-based simulation framework for scalable verification of mutual exclusion algorithms

This work develops a formal method for modelling and verifying mutual exclusion algorithms based on timed automata and Uppaal. Being based on model checking (MC), the approach is not scalable in the number N of processes due to the well-known problem of state explosions, which arises, e.g., for N ≥ 4 processes. Alternatively, the statistical model checker (SMC) of Uppaal can be used, which emulates concurrency and action non-determinism by stochastic behaviour. Although SMC permits studying a model for greater values of N, scalability problems can still be present due to data accumulation during the simulations. In this paper, a more efficient technique is proposed that is based on a lightweight, efficient, and control-based actor system. A Uppaal model is translated into Java with processes that are mapped onto actors and atomic actions that are realised by messages. The paper demonstrates the effectiveness of the actor-based approach through different case studies.