Verifying fault-tolerant Erlang programs

ABSTRACT

In this paper we target the verification of fault tolerant aspects of distributed applications written in Erlang. Erlang is unusual in several respects. First, it is one of a few functional languages that is used in industry. Secondly the programming language contains support for concurrency and distribution as well as including constructs for handling fault-tolerance.Erlang programmers, of course, mostly work with ready-made language components. Our approach to verification of fault tolerance is to verify systems built using two central components of most Erlang software, a generic server component with fault tolerance handling, and a supervisor component that restarts failed processes.To verify Erlang programs built using these components we automatically translate them into processes of the μCRL process algebra, generate their state spaces, and use a model checker to determine whether they satisfy correctness properties specified in the μ-calculus.The key observation of this paper is that, due to the usage of these higher-level design patterns (supervisors and generic servers) that structure process communication and fault recovery, the state space generated from a Erlang program, even with failures occurring, is relatively small, and can be generated automatically. Moreover the method is independent from the actual Erlang program studied, and is thus reusable.We demonstrate the approach in a case study where a server, built using the generic server component, implements a locking service for a number of client processes, and show that the server tolerates client failures.

REFERENCES

• 1: T. Arts, C. B. Earle, and J. J. Sánchez-Penas. Translating erlang to μcrl. In Fourth International Conference on Application of Concurrency to System Design, June 2004.
• 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: Thomas Arts , Thomas Noll, Verifying Generic Erlang Client-Server Implementations, Selected Papers from the 12th International Workshop on Implementation of Functional Languages, p.37-52, September 04-07, 2000
• 4: Thomas Arts , Juan José Sánchez Penas, Global scheduler properties derived from local restrictions, Proceedings of the 2002 ACM SIGPLAN workshop on Erlang, p.49-57, October 07-07, 2002, Pittsburgh, Pennsylvania [doi>10.1145/592849.592856]
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Roby, Bandera: a source-level interface for model checking Java programs, Proceedings of the 22nd international conference on Software engineering, p.762-765, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337625]
• 6: CWI. μmcrl: A language and tool set to study communicating processes with data, February 1999.
• 7: Building a better bug-trap. Economist Technology Quarterly, June 2003.
• 8: E. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. LICS, pages 267--278, 1986.
• 9: Jean-Claude Fernandez , Hubert Garavel , Alain Kerbrat , Laurent Mounier , Radu Mateescu , Mihaela Sighireanu, CADP - A Protocol Validation and Verification Toolbox, Proceedings of the 8th International Conference on Computer Aided Verification, p.437-440, August 03, 1996
• 10: H. Garavel, F. Lang, and R. Mateescu. An overview of cadp 2001. European Association for Software Science and Technology (EASST) Newsletter, 4:13--24, August 2002.
• 11: Jan F Groote, The syntax and semantics of timed $\mu CRL$, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1997
• 12: J. F. Groote, W. Fokking, and M. Reiniers. Modelling concurrent systems: Protocol verification in μCRL, April 2000.
• 13: K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. STTT, 2(4):366--381, March 2000.
• 14: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 15: Tomasz Janowski , Mathai Joseph, Dynamic Scheduling and Fault-Tolerance: Specification andVerification, Real-Time Systems, v.20 n.1, p.51-81, Jan. 2001 [doi>10.1023/A:1026537232278]
• 16: D. Kozen. Results on the propositional μ-calculus. TCS, 27:333--354, 1983.
• 17: R. Mateescu. Local model-checking of an alternation-free value-based modal mu-calculus. In Proceedings of the International Workshop on Software Tools for Technology Transfer STTT'98, Aalborg, Denmark, July 1998.
• 18: John Rushby, Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms, IEEE Transactions on Software Engineering, v.25 n.5, p.651-660, September 1999 [doi>10.1109/32.815324 ]
• 19: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 20: Juan José Sánchez Penas , Carlos Abalde Ramiro, Extending the VoDKA architecture to improve resource modelling, Proceedings of the 2003 ACM SIGPLAN workshop on Erlang, p.15-22, August 29-29, 2003, Uppsala, Sweden [doi>10.1145/940880.940883]
• 21: Francis Schneider , Steve Easterbrook , John R. Callahan , Gerard J. Holzmann, Validating Requirements for Fault Tolerant Systems using Model Checking, Proceedings of the 3rd International Conference on Requirements Engineering: Putting Requirements Engineering to Practice, p.4-13, April 06-10, 1998
• 22: Jaco van de Pol , Miguel Valero Espada, Formal Specification of JavaSpaces™ Architecture Using µCRL, Proceedings of the 5th International Conference on Coordination Models and Languages, p.274-290, April 08-11, 2002
• 23: A. G. Wouters. Manual for the μcrl tool set (version 2.8.2). Technical Report SEN-R0130, CWI, Amsterdam, 2001.

INDEX TERMS

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

General Terms:
Verification

Keywords:
code verification, concurrency, fault-tolerance