Sarir: A Rebeca to mCRL2 Translator (Tool Paper)

H. Hojjat, M. Sirjani, M.R. Mousavi, J.F. Groote. Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD'07), Bratislava, Slovak Republic, IEEE CS, July 2007.

Abstract

This paper describes a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation for the translation is to exploit the verification tools and theories developed for mCRL2 in Rebeca. The mapping is applied to several case-studies including the tree identify phase of the IEEE 1394. The results of the experiment show that the minimization tools of mCRL2 can be effective for model checking Rebeca and the present translation outperforms the translation to Promela, the input language of the Spin model-checker.

@InProceedings{MousaviAcsd07,
    author      = "Hojjat, H. and Sirjani, M. and Mousavi, M.R. and Groote, J.F.", 
    title       = "arir: A Rebeca to mCRL2 Translator",
    booktitle   = "Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD'07)",
    publisher   = "IEEE Computer Society Press, Los Alamitos, CA, USA, 2007"
}