Loading...

Modular verification of a component-based actor language

Sirjani, M ; Sharif University of Technology | 2005

200 Viewed
  1. Type of Document: Article
  2. DOI: 10.3217/jucs-011-10-1695
  3. Publisher: 2005
  4. Abstract:
  5. Rebeca is an actor-based 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 eventdriven 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. © J.UCS
  6. Keywords:
  7. Component ; Modular verification ; Reactive systems ; Rebeca ; The actor model
  8. Source: Journal of Universal Computer Science ; Volume 11, Issue 10 , 2005 , Pages 1695-1717 ; 0958695X (ISSN)
  9. URL: https://lib.jucs.org/articles.php?id=28493