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
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;
Conference_Titel :
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN :
0-7695-2077-4
DOI :
10.1109/CSD.2004.1309125
