JUCS - Journal of Universal Computer Science 11(6): 1054-1082, doi: 10.3217/jucs-011-06-1054
Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models
Marjan Sirjani‡, Ali Movaghar§, Amin Shali|, Frank S. De Boer¶‡ Department of Electrical and Computer Engineering, University of Tehran, Iran§ Department of Electrical and Computer Engineering, University of Tehran and School of Computer Science, IPM, Tehran, Iran| Department of Electrical and Computer Engineering, University of Tehran, Tehran, Iran¶ Department of Software Engineering, Centrum voor Wiskunde en Informatica, Amsterdam, Netherlands
Corresponding author: Marjan Sirjani ( msirjani@ut.ac.ir ) © Marjan Sirjani, Ali Movaghar, Amin Shali, Frank De Boer. This article is freely available under the J.UCS Open Content License. Citation:
Sirjani M, Movaghar A, Shali A, De Boer FS (2005) Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models. JUCS - Journal of Universal Computer Science 11(6): 1054-1082. https://doi.org/10.3217/jucs-011-06-1054 |  |
Abstract
Actor-based modeling, with encapsulated active objects which communicate asynchronously, is generally recognized to be well-suited for representing concurrent and distributed systems. In this paper we discuss the actor-based language Rebeca which is based on a formal operational interpretation of the actor model. Its Java-like syntax and object-based style of modeling makes it easy to use for software engineers, and its independent objects as units of concurrency leads to natural abstraction techniques necessary for model checking. We present a front-end tool for translating Rebeca to the languages of existing model checkers in order to model check Rebeca models. Automated modular verification and abstraction techniques are supported by the tool.
Keywords
actor model, reactive systems, model checking, modular verification, abstraction techniques