Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models
Дата
Авторы
Sirjani,Marjan
Movaghar,Ali
Shali,Amin
De Boer,Frank
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
actor model , reactive systems , model checking , modular verification , abstraction techniques