Verification of timed erlang/OTP components using the process algebra μcrl

ABSTRACT

Recent work has looked at how Erlang programs could be model-checked via translation into the process algebra μCRL. Rules for translating Erlang programs and OTP components into μCRL have been defined and investigated. However, in the existing work, no rule is defined for the translation of timeout events into μCRL. This could degrade the usability of the existing work as in some real applications, timeout events play a significant role in the system development. In this paper, by extending the existing work, we investigate the verification of timed Erlang/OTP components in μCRL. By using an explicit tick action in the μCRL specification, a discrete-time timing model is defined to support the translation of timed Erlang functions into μCRL. Two small examples are presented, which demonstrates the applications of the proposed approach.

REFERENCES

• 1: Joe Armstrong , Robert Virding , Claes Wikström , Mike Williams, Concurrent programming in ERLANG (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1996
• 2: Thomas Arts , Clara Benac Earle , John Derrick, Verifying Erlang Code: A Resource Locker Case-Study, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.184-203, July 22-24, 2002
• 3: T. Arts, C. Benac-Earle, and Juan José Sánchez Penas. Translating Erlang to μCRL. In The Fourth International Conference on Application of Concurrency to System Design (ACSD'04), pages 135--144. IEEE Computer Society, June 2004.
• 4: J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
• 5: C. Benac-Earle. Model checking the interaction of Erlang components. PhD thesis, The University of Kent, Canterbury, Department of Computer Science, 2006.
• 6: C. Benac-Earle and Lars-Åke Fredlund. Verification of Language Based Fault-Tolerance. In Roberto Moreno-Díaz, Franz Pichler, and Alexis Quesada-Arencibia, editors, EUROCAST, pages 140--149. Springer-Verlag, February 2005.
• 7: Clara Benac Earle , Lars-Åke Fredlund , John Derrick, Verifying fault-tolerant Erlang programs, Proceedings of the 2005 ACM SIGPLAN workshop on Erlang, September 26-28, 2005, Tallinn, Estonia [doi>10.1145/1088361.1088367]
• 8: S. Blom, N. Ioustinova, and N. Sidorova. Timed verification with μCRL. In Manfred Broy and Alexandre V. Zamulin, editors, 5th Andrei Ershov International Conference on Perspectives of System Informatics PSI'2003, volume 2890 of LNCS, pages 178--192. Springer-Verlag, July 2003.
• 9: Tommaso Bolognesi , Ed Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, v.14 n.1, p.25-59, March, 1987 [doi>10.1016/0169-7552(87)90085-7]
• 10: CADP. http://www.inrialpes.fr/vasy/cadp/.
• 11: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 12: Lars-Åke Fredlund, D. Gurov, T. Noll, M. Dam, T. Arts, and G. Chugunov. A verification tool for Erlang. International Journal on Software Tools for Technology Transfer, 4(4):405--420, August 2003.
• 13: Jan F Groote, The syntax and semantics of timed $\mu CRL$, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1997
• 14: J. F. Groote and A. Ponse. The syntax and sematics of μCRL. In Algebra of Communicating Processes 1994, Workshop in Computing, pages 26--62, 1995.
• 15: Q. Guo. Verifying Erlang/OTP Components in μCRL. In John Derrick and Jüri Vain, editors, FORTE'07, volume 4574 of LNCS, pages 227--246. Springer-Verlag, June 2007.
• 16: Q. Guo and J. Derrick. Eliminating overlapping of pattern matching when verifying Erlang programs in μCRL. In 12th International Erlang User Conference (EUC'06), Stockholm, Sweden, 2006.
• 17: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 18: Frank Huch, Verification of Erlang programs using abstract interpretation and model checking, ACM SIGPLAN Notices, v.34 n.9, p.261-272, Sept. 1999
• 19: D. Kozen. Results on the propositional μ-calculus. Theortical Computer Science, 27:333--354, 1983.
• 20: K. Larsen, P. Pettersson, and W. Yi. UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2):134--152, October 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
OTP, erlang, process algebra μCRL, timeout events, verification