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

Chryssis Georgiou, Peter M. Musial, Alexander A. Shvartsman, Elaine L. Sonderegger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationPODC'07
Subtitle of host publicationProceedings of the 26th Annual ACM Symposium on Principles of Distributed Computing
Pages334-335
Number of pages2
DOIs
StatePublished - 2007
Externally publishedYes
EventPODC'07: 26th Annual ACM Symposium on Principles of Distributed Computing - Portland, OR, United States
Duration: Aug 12 2007Aug 15 2007

Publication series

NameProceedings of the Annual ACM Symposium on Principles of Distributed Computing

Conference

ConferencePODC'07: 26th Annual ACM Symposium on Principles of Distributed Computing
Country/TerritoryUnited States
CityPortland, OR
Period8/12/078/15/07

Keywords

  • Asynchronous communication
  • Dynamic participation
  • I/O automata
  • TCP and Java sockets

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Brief announcement: A formal treatment of an abstract channel implementation using java sockets and TCP'. Together they form a unique fingerprint.

Cite this