Statistical Model Checking for P

P is a programming language equipped with a unified framework for modeling, specifying, implementing, testing, and verifying complex distributed systems. This language is based on the actor model, and its framework includes a compiler toolchain for code generation, bounded randomized testing, and reachability analysis. This paper presents an extension of P ’s framework to include statistical model checking of quantititive temporal logic formulas. The distributed statistical model checking for discrete event simulators has been integrated into the P framework for Monte Carlo validation of P programs against QuaTEx quantitative temporal logic formulas. For this, P ’s compiler has been modified to generate instrumentation code enabling the observation of a program’s attributes without direct, manual intervention of the code. As a result, distributed incremental statistical model checking is now available for P via probabilistic sampling. As the experiments show, some of them reported here, these new verification capabilities scale up and complement the ones already available for P.