In this paper, we propose extended Rebeca as a toolsupported 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.