Slicing-based Reductions for Rebeca

Slicing is a program analysis technique which can be used for reducing the size of the model and avoid state explosion in model checking. In this work a static slicing technique is proposed for reducing Rebeca models with respect to a property. For applying the slicing techniques, the Rebeca dependence graph (RDG) is introduced. As the static slicing usually produces large slices, two other slicing-based reduction techniques, step-wise slicing and bounded slicing, are proposed as simple novel ideas. Step-wise slicing first generates slices overapproximating the behavior of the original model and then refines it, and bounded slicing is based on the semantics of non-deterministic assignments in Rebeca. We also propose a static slicing algorithm for deadlock detection (in absence of any particular property). The applicability of these techniques is checked by applying them to several case studies which are included in this paper. Similar techniques can be applied on the other actor-based languages.