TY - GEN
T1 - An abstract channel specification and an algorithm implementing it using Java sockets
AU - Georgiou, Chryssis
AU - Shvartsman, Alexander A.
AU - Musial, Peter M.
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 - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=51749104408&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=51749104408&partnerID=8YFLogxK
U2 - 10.1109/NCA.2008.12
DO - 10.1109/NCA.2008.12
M3 - Conference contribution
AN - SCOPUS:51749104408
SN - 9780769531922
T3 - Proceedings of the 7th IEEE International Symposium on Networking Computing and Applications, NCA 2008
SP - 211
EP - 219
BT - Proceedings of the 7th IEEE International Symposium on Networking Computing and Applications, NCA 2008
T2 - 7th IEEE International Symposium on Networking Computing and Applications, NCA 2008
Y2 - 10 July 2008 through 12 July 2008
ER -