Affiliations: Department of Computer Engineering, Sharif University
of Technology, Azadi Ave., Tehran, Iran | Department of Electrical and Computer Engineering,
University of Tehran, Karegar Ave., Tehran, Iran | Department of Software Engineering, CWI, Kruislaan
413, 1098 SJ, Amsterdam, The Netherlands
Abstract: 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.
Keywords: actor model, reactive systems, model checking, compositional verification, property preserving abstraction
