View article

Rebeca is an actor-based language with formal semantics that can be used in modeling concurrent and distributed software and protocols. Automatic verification of these systems in the design stage helps develop error free systems. In this paper, we describe the model checking tool developed for verification of Rebeca models. This tool uses partial order reduction technique for reducing the size of the state space generated for a given model. Using this tool for model checking Rebeca yields much better results than the previous attempts for model checking Rebeca.