Abstract
Erlang is a concurrent functional programming language with explicit support for real-time and fault-tolerant distributed systems. Generic components encapsulated as design patterns are provided by the Open Telecom Platform (OTP) library. Although Erlang has many high-level features, verification is still non-trivial. One (existing) approach is to perform an abstraction of an Erlang program into the process algebra μCRL, upon which standard verification tools can be applied. In this paper we extend this work and propose a model that supports the translation of an OTP finite state machine design pattern into a μCRL specification. Then a standard toolset such as CADP can be applied in order to check properties that should hold for the system under development. Two small examples are presented, which experimentally show how the proposed model assists in model checking Erlang OTP components in μCRL.
Chapter PDF
References
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang, 2nd edn. Prentice-Hall, Englewood Cliffs (1996)
Arts, T., Benac, C.: 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: Proceedings of the Fourth International Conference on Application of Concurrency to System Design (ACSD’04), pp. 135–144 (2004)
Blau, J., Rooth, J., Axell, J., Hellstrand, F., Buhrgard, M., Westin, T., Wicklund, G.: AXD 301: A new generation ATM switching system. Computer Networks 31, 559–582 (1999)
Benac Earle, C.: Model check the interaction of Erlang components. PhD thesis, The University of Kent, Canterbury, Department of Computer Science (2006)
Fredlund, L.-A., Benac Earle, C., 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)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
Benac Earle, C., Fredlund, L.-A.: Verification of Language Based Fault-Tolerance. In: EUROCAST, pp. 140–149 (2005)
Huch, F.: Verification of Erlang programs using abstract interpretation and model checking. ACM SIGPLAN Notices 34(9), 261–272 (1999)
Fredlund, L.-A., Gurov, D., Noll, T., Dam, M., Arts, T., Chugunov, G.: A verification tool for Erlang. International Journal on Software Tools for Technology Transfer 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)
Baeten, J.C.M., Bergstra, J.A.: Process algebra with signals and conditions. Report P9008, University of Amsterdam (1990)
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, Cambridge (1990)
Guo, Q., Derrick, J.: Eliminating overlapping of pattern matching when verifying Erlang programs in μCRL. In: The 12th International Erlang User Conference (EUC‘06), Stockholm, Sweden (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Guo, Q. (2007). Verifying Erlang/OTP Components in μCRL. In: Derrick, J., Vain, J. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2007. FORTE 2007. Lecture Notes in Computer Science, vol 4574. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73196-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-73196-2_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73195-5
Online ISBN: 978-3-540-73196-2
eBook Packages: Computer ScienceComputer Science (R0)