Introduction

rbsc is a tool for the verification and quantitative analysis of role-based systems by means of probabilistic model checking. It provides a modeling language that extends the input language of the probabilistic model checker PRISM with role-related concepts. The rbsc tool is not a probabilistic model checker. Rather, it translates a role-based model into the PRISM language. Then, PRISM can be used for carrying out the quantitative analysis.

A role-based model described in the role-based modeling language RBL consists of a set of components. A component can either be a natural, a role or a compartment. Naturals are the atomic components that serve as players for roles. A compartment represents a context, in which a set of roles is acting in.