Translating Erlang to μCRL

Author

Arts, Thomas ; Earle, Clara Benac ; Penas, Juan José Sánchez

Author_Institution

Gothenburg IT Univ., Sweden

fYear

2004

fDate

16-18 June 2004

Firstpage

135

Lastpage

144

Abstract

The language Erlang has been developed by Ericsson to implement large switching systems. Erlang is nowadays used by several companies for complex embedded systems. The language μCRL is a process algebra with data. Several verification tools are available for μCRL and other process algebras, including a tool to create labelled transition systems from μCRL specifications. By having a translation from Erlang to μCRL we can apply the verification tools for process algebras and labelled transition systems to industrial code. The translation is aware of the major design component in the switching software. This knowledge is used to ensure that the size of the labelled transition system generated by the tools is smaller than with a naive translation.

Keywords

embedded systems; formal specification; functional languages; functional programming; process algebra; program interpreters; program verification; telecommunication computing; telecommunication switching; μCRL language; μCRL specifications; Erlang language translation; complex embedded systems; design component; industrial code; labelled transition systems; process algebra; switching software; switching systems; verification tools; Algebra; Asynchronous transfer mode; Concurrent computing; Functional programming; Object oriented modeling; Software performance; Software safety; Software tools; State-space methods; Switches;

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.1309124

Filename

1309124