Modular Verification of a Component-Based Actor Language
Дата
Авторы
Sirjani,Marjan
De Boer,Frank
Movaghar,Ali
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
actor model , reactive systems , Rebeca , component , modular verification