Extended Rebeca: a component-based actor language with synchronous message passing

In this paper, we propose extended Rebeca as a tool-supported actor-based language for modeling and verifying concurrent and distributed systems. We enrich Rebeca with a formal concept of components which integrates the message-driven computational model of actor-based languages with synchronous message passing. Components are used to encapsulate a set of internal active objects which react asynchronously to messages by means of methods and which additionally interact via a synchronous message passing mechanism. Components themselves interact only via asynchronous and anonymous messages. We present our compositional verification approach and abstraction techniques, and the theory corresponding to it, based on the formal semantics of Rebeca. These techniques are exploited to overcome the state explosion problem in model checking.