Advertisement

Verifying Erlang Telecommunication Systems with the Process Algebra μCRL

  • Qiang Guo
  • John Derrick
  • Csaba Hoch
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)

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.

Keywords

Erlang Telecoms case study Process Algebras μCRL Translation Verification 

References

  1. 1.
    Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang, 2nd edn. Prentice-Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, Cambridge (1990)CrossRefzbMATHGoogle Scholar
  5. 5.
    Benac-Earle, C.: Model checking the interaction of Erlang components. PhD thesis, The University of Kent, Canterbury, Department of Computer Science (2006)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
  9. 9.
    Clarke, E., Grumberg, O., Long, D.: Model Checking. MIT Press, Cambridge (1999)zbMATHGoogle Scholar
  10. 10.
    Fredlund, L.Å: Towards a sematics for Erlang. In: Foundatins of Mobile Computation: A Post-Conference Satellite Workshop of FST and TCS (1999)Google Scholar
  11. 11.
    Fredlund, L.-Å.: A Framework for Reasoning about Erlang Code. PhD thesis, Roral Institute of Technology, Stockholm, Sweden (2001)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Groote, J.F., Ponse, A.: The syntax and sematics of μCRL. In: Algebra of Communicating Processes 1994, Workshop in Computing, pp. 26–62 (1995)Google Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Guo, Q., Derrick, J.: Eliminating overlapping of pattern matching when verifying Erlang programs in μCRL. In: Sha, E., Han, S.-K., Xu, C.-Z., Kim, M.-H., Yang, L.T., Xiao, B. (eds.) EUC 2006. LNCS, vol. 4096, Springer, Heidelberg (2006)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Huch, F.: Verification of Erlang programs using abstract interpretation and model checking. ACM SIGPLAN Notices 34(9), 261–272 (1999)CrossRefzbMATHGoogle Scholar
  18. 18.
    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)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Qiang Guo
    • 1
  • John Derrick
    • 1
  • Csaba Hoch
    • 2
  1. 1.Department of Computer ScienceThe University of SheffieldPortobelloUK
  2. 2.Faculty of InformaticsEötvös Loránd TudományegyetemBudapestHungary

Personalised recommendations