Modeling and Verification of Probabilistic Actor Systems Using pRebeca

摘要

Quantitative verification has gained an increasing attention as a promising approach for analysis of systems in various domains, especially for distributed systems, where the uncertainties of the environment cause the system to exhibit probabilistic and nondeterministic behavior. In this paper, we introduce pRebeca, an extension to the high-level actor-based modeling language Rebeca, that is used to model distributed and reactive systems with probabilistic and nondeterministic nature. We propose a simple syntax suitable for describing different aspects of a probabilistic system behavior and provide a formal semantics based on Markov decision processes. To model check a pRebeca model, it is converted to a Markov decision process and verified using the PRISM model checker against PCTL properties. Using a couple of examples, we show how a probabilistic system can be expressed in pRebeca in a simple way, while taking advantage of the PRISM model checker features.