Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang, 2nd edn. Prentice-Hall, Englewood Cliffs (1996)
Arts, T., Benac-Earle, C., Derrick, J.: Verifying Erlang code: a resource locker case-study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 184–203. Springer, Heidelberg (2002)
Arts, T., Benac-Earle, C., Penas, J.J.S.: Translating Erlang to μCRL. In: The Fourth International Conference on Application of Concurrency to System Design (ACSD 2004), June 2004, pp. 135–144. IEEE Computer Society, Los Alamitos (2004)
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, Cambridge (1990)
Benac-Earle, C.: Model checking the interaction of Erlang components. PhD thesis, The University of Kent, Canterbury, Department of Computer Science (2006)
Benac-Earle, C., Fredlund, L.-Å.: Verification of Language Based Fault-Tolerance. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2005. LNCS, vol. 3643, pp. 140–149. Springer, Heidelberg (2005)
Benac-Earle, C., Fredlund, L.-Å., Derrick, J.: Verifying Fault-Tolerant Erlang Programs. In: Sagonas, K., Armstrong, J. (eds.) Proceedings of ACM SigPlan Erlang 2005 Workshop, pp. 26–34. ACM Press, New York (2005)
Clarke, E., Grumberg, O., Long, D.: Model Checking. MIT Press, Cambridge (1999)
Fredlund, L.Å: Towards a sematics for Erlang. In: Foundatins of Mobile Computation: A Post-Conference Satellite Workshop of FST and TCS (1999)
Fredlund, L.-Å.: A Framework for Reasoning about Erlang Code. PhD thesis, Roral Institute of Technology, Stockholm, Sweden (2001)
Fredlund, L.-Å., Gurov, D., Noll, T., Dam, M., Arts, T., Chugunov, G.: A verification tool for Erlang. International Journal on Software Tools for Technology Transfer 4(4), 405–420 (2003)
Groote, J.F., Ponse, A.: The syntax and sematics of μCRL. In: Algebra of Communicating Processes 1994, Workshop in Computing, pp. 26–62 (1995)
Guo, Q.: Verifying Erlang/OTP Components in μCRL. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574. pp. 227–246. Springer, Heidelberg (2007)
Guo, Q., Derrick, J.: Eliminating overlap** of pattern matching when verifying Erlang programs in μCRL. In: Sha, E., Han, S.-K., Xu, C.-Z., Kim, M.-H., Yang, L.T., **%20of%20pattern%20matching%20when%20verifying%20Erlang%20programs%20in%20%CE%BCCRL&publication_year=2006&author=Guo%2CQ.&author=Derrick%2CJ."> Google Scholar
Guo, Q., Derrick, J.: Verification of Timed Erlang/OTP Components Using the Process Algebra μCRL. In: Thompson, S., Fredlund, L.-A. (eds.) 6th ACM SIGPLAN Erlang Workshop, pp. 55–64. ACM Press, New York (2007)
Huch, F.: Verification of Erlang programs using abstract interpretation and model checking. ACM SIGPLAN Notices 34(9), 261–272 (1999)
Svensson, H., Fredlund, L.-ȦA.: A More Accurate Semantics for Distributed Erlang. In: Thompson, S., Fredlund, L.-A. (eds) 6th ACM SIGPLAN Erlang Workshop, pp. 43–54. ACM Press, New York (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Guo, Q., Derrick, J., Hoch, C. (2008). Verifying Erlang Telecommunication Systems with the Process Algebra μCRL. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2008. FORTE 2008. Lecture Notes in Computer Science, vol 5048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68855-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-68855-6_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68854-9
Online ISBN: 978-3-540-68855-6
eBook Packages: Computer ScienceComputer Science (R0)