Sarir: a Rebeca to mCRL2 translator

H. Hojjat; M. Sirjani; M. Mousavi; J.F. Groote

doi:10.1109/ACSD.2007.24

Sarir: a Rebeca to mCRL2 translator

H. Hojjat
, M. Sirjani
, M. Mousavi
, J.F. Groote

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

7 Citations (Scopus)

Abstract

We describe a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation 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 standard. The results of the experiment show that the minimization tools of mCRL2 can be very effective and the outcome of the present translation outperforms that of the translation to the input language of the Spin model-checker.

Original language	English
Title of host publication	Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD '07) 10-13 July 2007, Bratislava, Slovak Republic
Publisher	IEEE Computer Society
Pages	216-222
ISBN (Print)	0-7695-2363-3
DOIs	https://doi.org/10.1109/ACSD.2007.24
Publication status	Published - 2007
Event	7th International Conference on Application of Concurrency to System Design (ACSD 2007) - Bratislava, Slovakia Duration: 10 Jul 2007 → 13 Jul 2007 Conference number: 7

Conference

Conference	7th International Conference on Application of Concurrency to System Design (ACSD 2007)
Abbreviated title	ACSD 2007
Country/Territory	Slovakia
City	Bratislava
Period	10/07/07 → 13/07/07

Access to Document

10.1109/ACSD.2007.24

Cite this

@inproceedings{c50ba8b6fa994884a6c9a27a5e8d2da2,

title = "Sarir: a Rebeca to mCRL2 translator",

abstract = "We describe a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation 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 standard. The results of the experiment show that the minimization tools of mCRL2 can be very effective and the outcome of the present translation outperforms that of the translation to the input language of the Spin model-checker.",

author = "H. Hojjat and M. Sirjani and M. Mousavi and J.F. Groote",

year = "2007",

doi = "10.1109/ACSD.2007.24",

language = "English",

isbn = "0-7695-2363-3",

pages = "216--222",

booktitle = "Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD '07) 10-13 July 2007, Bratislava, Slovak Republic",

publisher = "IEEE Computer Society",

address = "United States",

note = "7th International Conference on Application of Concurrency to System Design (ACSD 2007), ACSD 2007 ; Conference date: 10-07-2007 Through 13-07-2007",

}

Hojjat, H, Sirjani, M, Mousavi, M & Groote, JF 2007, Sarir: a Rebeca to mCRL2 translator. in Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD '07) 10-13 July 2007, Bratislava, Slovak Republic. IEEE Computer Society, pp. 216-222, 7th International Conference on Application of Concurrency to System Design (ACSD 2007), Bratislava, Slovakia, 10/07/07. https://doi.org/10.1109/ACSD.2007.24

Sarir: a Rebeca to mCRL2 translator. / Hojjat, H.; Sirjani, M.; Mousavi, M. et al.
Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD '07) 10-13 July 2007, Bratislava, Slovak Republic. IEEE Computer Society, 2007. p. 216-222.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Sarir: a Rebeca to mCRL2 translator

AU - Hojjat, H.

AU - Sirjani, M.

AU - Mousavi, M.

AU - Groote, J.F.

N1 - Conference code: 7

PY - 2007

Y1 - 2007

N2 - We describe a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation 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 standard. The results of the experiment show that the minimization tools of mCRL2 can be very effective and the outcome of the present translation outperforms that of the translation to the input language of the Spin model-checker.

AB - We describe a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation 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 standard. The results of the experiment show that the minimization tools of mCRL2 can be very effective and the outcome of the present translation outperforms that of the translation to the input language of the Spin model-checker.

U2 - 10.1109/ACSD.2007.24

DO - 10.1109/ACSD.2007.24

M3 - Conference contribution

SN - 0-7695-2363-3

SP - 216

EP - 222

BT - Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD '07) 10-13 July 2007, Bratislava, Slovak Republic

PB - IEEE Computer Society

T2 - 7th International Conference on Application of Concurrency to System Design (ACSD 2007)

Y2 - 10 July 2007 through 13 July 2007

ER -

Sarir: a Rebeca to mCRL2 translator

Abstract

Conference

Access to Document

Fingerprint

Cite this