An abstract channel specification and an algorithm implementing it using Java sockets

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

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

2 Scopus citations

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 often negated by the ad hoc process of mapping the semantics of an abstract specification to algorithms designed to be executed on target distributed platforms. The challenge of formally specifying communication channels and correctly implementing them as algorithms that use realistic distributed system services is the focus of this paper. This work provides an original formal specification of an abstract asynchronous communication channel with support for dynamic creation and tear down of links between participating network nodes, and its implementation as an algorithm using Java sockets. The specification and the algorithm are expressed using the Input/Output Automata formalism, and it is proved that the algorithm correctly implements the specification, viz. that any externally observable behavior (trace) of the algorithm has a corresponding behavior of the specification. The approach presented here can be used to implement algorithms for dynamic systems, where communicating nodes may join, leave, and experience delays. The result is also of direct benefit to automated code generation, such as that implemented within the Input/Output Automata Toolkit at MIT.

Original languageEnglish (US)
Title of host publicationProceedings of the 7th IEEE International Symposium on Networking Computing and Applications, NCA 2008
Pages211-219
Number of pages9
DOIs
StatePublished - 2008
Externally publishedYes
Event7th IEEE International Symposium on Networking Computing and Applications, NCA 2008 - Cambridge, MA, United States
Duration: Jul 10 2008Jul 12 2008

Publication series

NameProceedings of the 7th IEEE International Symposium on Networking Computing and Applications, NCA 2008

Conference

Conference7th IEEE International Symposium on Networking Computing and Applications, NCA 2008
Country/TerritoryUnited States
CityCambridge, MA
Period7/10/087/12/08

ASJC Scopus subject areas

  • Computer Science Applications
  • Hardware and Architecture

Fingerprint

Dive into the research topics of 'An abstract channel specification and an algorithm implementing it using Java sockets'. Together they form a unique fingerprint.

Cite this