A formal treatment of an abstract channel implementation using java sockets and TCP

ABSTRACT

Abstract models and specifications can be used in the design of distributed applications to formally reason about their safety properties. However, the benefits of using formal methods are offset by the challenging process of mapping the functionality of an abstract specification to the low-level executable code for target distributed platforms. Formal specification and practical implementation of communication channels is one such challenge. This work provides the first formal specification of an abstract asynchronous communication channel with support for dynamic creation and tear down of communication links between participating network nodes, and its implementation using Java sockets and TCP. The specifications are formulated using Input/Output Automata formalism, and it is proved that the resulting implementation preserves the safety properties of the abstract channel. The approach presented here can be used to implement algorithms for dynamic systems, where communicating nodes may join, leave, and experience arbitrary delays, and it can directly benefit automated code generation.

REFERENCES

• 1: Tempo toolset. http://www.veromodo.com, VeroModo Inc., 2006.
• 2: S. Garland and N. Lynch. The IOA language and toolset: Support for designing, analyzing, and building distributed systems. Technical Report MIT/LCS/TR-762, MIT, 1998.
• 3: S. Garland, N. Lynch, and M. Vaziri. IOA: A language for specifying, programming, and validating distributed systems, 2001.
• 4: C. Georgiou, N. Lynch, P. Mavrommatis, and J. A. Tauber. Automated implementation of complex distributed algorithms specified in the IOA language. In Proc. of the 18th International Conference on Parallel and Distributed Computing Systems, pages 128--134, 2005.
• 5: C. Georgiou, P. Musial, A. Shvartsman, and E. Sonderegger. A Formal Treatment of an Abstract Channel Implementation Using Java Sockets. Technical Report BECAT/CSE-TR-06-10, University of Connecticut, 2006.
• 6: P. Hatziprocopiou. Automated implementation of the Paxos algorithm using the IOA toolkit. BSc Thesis, University of Cyprus, June 2006.
• 7: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 8: N. Lynch and M. Tuttle. An introduction to Input/Output Automata. CWI-Quarterly, 2(3):219--246, 1989.
• 9: Nancy Lynch , Frits Vaandrager, Forward and backward simulations I.: untimed systems, Information and Computation, v.121 n.2, p.214-233, Sept. 1995 [doi>10.1006/inco.1995.1134]
• 10: Message Passing Interface Forum. MPI: A Message-Passing Interface standard. The International Journal of Supercomputer Applications and High Performance Computing, 8, 1994.
• 11: J. Postel. DARPA Internet program specification (internet standard stc--007). Internet RFC-793, September 1981.
• 12: Sun Microsystems. JavaTM Platform SE 6. http://java.sun.com/javase/6/docs/api/.
• 13: Joshua A. Tauber , Nancy A. Lynch, Verifiable compilation of i/o automata without global synchronization, Massachusetts Institute of Technology, Cambridge, MA, 2005

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

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

General Terms:
Design, Verification

Keywords:
I/O automata, TCP and java sockets, asynchronous communication, dynamic participation