JUCS - Journal of Universal Computer Science 11(10): 1695-1717, doi: 10.3217/jucs-011-10-1695
Modular Verification of a Component-Based Actor Language
expand article infoMarjan Sirjani, Frank S. De Boer§, Ali Movaghar|
‡ Department of Electrical and Computer Engineering, University of Tehran, Iran§ Department of Software Engineering, Centrum voor Wiskunde en Informatica, Amsterdam, Netherlands| School of Computer Science, IPM, Tehran, Iran
Open Access
Rebeca is an actor­based language for modeling concurrent and distributed systems as a set of reactive objects which communicate via asynchronous message passing. Rebeca is extended to support synchronous communication, and at the same time components are introduced to encapsulate the tightly coupled reactive objects which may communicate by synchronous messages. This provide us a language for modeling globally asynchronous and locally synchronous systems. Components interact only by asynchronous messages. This feature and also the event-driven nature of the computation are exploited to introduce a modular verification approach in order to overcome the state explosion problem in model checking. In this paper we elaborate on the corresponding theory of the modular verification approach which is based on the formal semantics of components in extended Rebeca.
actor model, reactive systems, Rebeca, component, modular verification