Show simple item record

dc.contributor.authorGeorgiou, Chryssisen
dc.contributor.authorMusiał, Peter M.en
dc.contributor.authorShvartsman, A. A.en
dc.contributor.authorSonderegger, E. L.en
dc.creatorGeorgiou, Chryssisen
dc.creatorMusiał, Peter M.en
dc.creatorShvartsman, A. A.en
dc.creatorSonderegger, E. L.en
dc.description.abstractAbstract 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. Copyright © 2007 ACM.en
dc.sourceProceedings of the Annual ACM Symposium on Principles of Distributed Computingen
dc.sourcePODC'07: 26th Annual ACM Symposium on Principles of Distributed Computingen
dc.subjectNetwork protocolsen
dc.subjectAutomata theoryen
dc.subjectChannel estimationen
dc.subjectSystems analysisen
dc.subjectJava programming languageen
dc.subjectAsynchronous communicationen
dc.subjectDynamic participationen
dc.subjectI/O automataen
dc.subjectJava socketsen
dc.subjectTCP and Java socketsen
dc.titleBrief announcement: A formal treatment of an abstract channel implementation using java sockets and TCPen
dc.description.endingpage335 Σχολή Θετικών και Εφαρμοσμένων Επιστημών / Faculty of Pure and Applied SciencesΤμήμα Πληροφορικής / Department of Computer Science
dc.type.uhtypeConference Objecten
dc.description.notes<p>Sponsors: ACM SIG on Operating Systemsen
dc.description.notesACM SIG on Algorithms and Computation Theoryen
dc.description.notesConference code: 70700</p>en
dc.contributor.orcidGeorgiou, Chryssis [0000-0003-4360-0260]

Files in this item


There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record