Rebeca is an actor-based language for modeling concurrent and reactive systems with asynchronous message passing. The actor model was originally introduced by Hewitt as an agent-based language, and is a mathematical model of concurrent computation that treats as the universal primitives of concurrent computation. A Rebeca model is similar to the actor model as it has reactive objects with no shared variables, asynchronous message passing with no blocking send and no explicit receive, and unbounded buffers for messages. Objects in Rebeca are reactive, self-contained, and each of them is called a rebec (reactive object). Communication takes place by message passing among rebecs. Each rebec has an unbounded buffer, called message queue, for its arriving messages. Computation is event-driven, meaning that each rebec takes a message that can be considered as an event from the top of its message queue and execute the corresponding message server (also called a method). The execution of a message server is atomic execution (non-preemptive execution) of its body that is not interleaved with any other method execution.
Marjan Sirjani, Ali Movaghar, Hamed Iravanchi, Mohammad Mahdi Jaghoori, Amin Shali: Model Checking in Rebeca. PDPTA 2003: 1819-1822. [bib]
Marjan Sirjani, Ali Movaghar, Amin Shali, Frank S. de Boer: Modeling and Verification of Reactive Systems using Rebeca. Fundam. Inform. 63(4): 385-410 (2004). [pdf] [bib]
Ehsan Khamespanah, Marjan Sirjani, Ramtin Khosravi: Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family Models. FSEN 2023: 72-87. [pdf] [bib]