TY - GEN
T1 - A formal treatment of an abstract channel implementation using java sockets and TCP.
T2 - PODC'07: 26th Annual ACM Symposium on Principles of Distributed Computing
AU - Georgiou, Chryssis
AU - Musial, Peter M.
AU - Shvartsman, Alexander A.
AU - Sonderegger, Elaine L.
N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
KW - Asynchronous communication
KW - Dynamic participation
KW - I/O automata
KW - TCP and Java sockets
UR - http://www.scopus.com/inward/record.url?scp=36849046765&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=36849046765&partnerID=8YFLogxK
U2 - 10.1145/1281100.1281159
DO - 10.1145/1281100.1281159
M3 - Conference contribution
AN - SCOPUS:36849046765
SN - 1595936165
SN - 9781595936165
T3 - Proceedings of the Annual ACM Symposium on Principles of Distributed Computing
SP - 334
EP - 335
BT - PODC'07
Y2 - 12 August 2007 through 15 August 2007
ER -