Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their correctness. In this paper, we develop an actor-based model for describing such systems, use temporal logic to specify properties of the model, and apply different abstraction and verification methods for verifying that the model meets its specification. We use a compositional verification approach for verifying safety properties of these models. For that we introduce a notion of component, based on an user-defined decomposition of the model. Components are more abstract than the model itself, and so we can reduce the state space of the model which makes it more amenable to model checking techniques. We prove that our abstraction technique preserves a set of behavioral specifications in temporal logic. The soundness of the abstraction is proved by the weak simulation relation between the constructs.