-

Abstract

By increasing use of concurrent systems, especially in critical applications, we need a proper model for specifying these systems in a reliable way. In this paper, we propose an actor-based language for modeling concurrent systems and present its operational semantics in basic transition system. The model consists of independent reactive objects which communicate via asynchronous message passing. Dynamic creation of reactive objects and dynamic changing topology are two features of the model. The proposed language and its formal semantics have been a basis for developing an automated tool for modeling and verifying reactive systems.