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
Marjan 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
Corresponding author: Marjan Sirjani ( msirjani@ut.ac.ir ) © Marjan Sirjani, Frank De Boer, Ali Movaghar. This article is freely available under the J.UCS Open Content License. Citation:
Sirjani M, De Boer FS, Movaghar A (2005) Modular Verification of a Component-Based Actor Language. JUCS - Journal of Universal Computer Science 11(10): 1695-1717. https://doi.org/10.3217/jucs-011-10-1695 |  |
Abstract
Rebeca is an actorbased 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.
Keywords
actor model, reactive systems, Rebeca, component, modular verification