Verifying Erlang Telecommunication Systems with the Process Algebra μCRL

摘要

Verification is an important process in the development of Erlang systems. A recent strand of work has studied the verification of Erlang applications using the process algebra μCRL. The general idea is that Erlang programs are translated into a μCRL specification, upon which the standard model checkers can be applied for checking the system's properties. In this paper, we pull together some of the existing work and investigate the verification of an Erlang telecommunication system in μCRL. This case study uses a server-client structure and incorporates timing restrictions and is designed and implemented using a number of Erlang/OTP components. We show how this system is translated into a μCRL specification by using the defined rules, after which system properties are checked via the toolset CADP. Through studying the verification of such an application, we aim to validate the effectiveness of the translation rules in an integrated way.