Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models

Marjan Sirjani (Department of Electrical and Computer Engineering, University of Tehran and School of Computer Science, IPM, Iran)

Ali Movaghar (Department of Electrical and Computer Engineering, University of Tehran and School of Computer Science, IPM, Iran)

Amin Shali (Department of Electrical and Computer Engineering, University of Tehran, Iran)

Frank S. de Boer (Department of Software Engineering, Centrum voor Wiskunde en Informatica, Netherlands)

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: abstraction techniques, actor model, model checking, modular verification, reactive systems

Categories: D.2.2, D.2.4