DocumentCode
3114649
Title
A front-end tool for automated abstraction and modular verification of actor-based models
Author
Sirjani, Marjan ; Shali, Amin ; Jaghoori, Mohammad Mahdi ; Iravanchi, Hamed ; Movaghar, Ali
fYear
2004
fDate
16-18 June 2004
Firstpage
145
Lastpage
148
Abstract
Actor-based modeling is known to be an appropriate approach for representing concurrent and distributed systems. Rebeca is an actor-based language with a formal foundation, based on an operational interpretation of the actor model. We develop a front-end tool for translating a subset of Rebeca to SMV in order to model check Rebeca models. Automated modular verification and abstraction techniques are supported by the tool.
Keywords
formal verification; multiprocessing programs; object-oriented languages; object-oriented programming; program interpreters; Rebeca language; Rebeca model; SMV; actor-based language; actor-based modeling; automated modular abstraction; automated modular verification; concurrent system; distributed system; front-end tool; model checking; Appropriate technology; Communication system control; Computational modeling; Concurrent computing; Distributed computing; Formal verification; Message passing; State-space methods; Topology; Yarn;
fLanguage
English
Publisher
ieee
Conference_Titel
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN
0-7695-2077-4
Type
conf
DOI
10.1109/CSD.2004.1309125
Filename
1309125
Link To Document