Show simple item record

dc.contributor.authorGeorgiou, Chryssisen
dc.contributor.authorShvartsman, A. A.en
dc.contributor.authorMusiał, Peter M.en
dc.contributor.authorSonderegger, E. L.en
dc.creatorGeorgiou, Chryssisen
dc.creatorShvartsman, A. A.en
dc.creatorMusiał, Peter M.en
dc.creatorSonderegger, E. L.en
dc.description.abstractModels 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. © 2008 IEEE.en
dc.sourceProceedings of the 7th IEEE International Symposium on Networking Computing and Applications, NCA 2008en
dc.source7th IEEE International Symposium on Networking Computing and Applications, NCA 2008en
dc.subjectInformation theoryen
dc.subjectComputer networksen
dc.subjectAutomata theoryen
dc.subjectTranslation (languages)en
dc.subjectTechnical presentationsen
dc.subjectCommunication channels (information theory)en
dc.subjectInternational symposiumen
dc.subjectConformal mappingen
dc.subjectBoolean functionsen
dc.subjectComputer programming languagesen
dc.subjectInput/output automataen
dc.subjectFormal methodsen
dc.subjectJava socketsen
dc.titleAn abstract channel specification and an algorithm implementing it using Java socketsen
dc.description.endingpage219 Σχολή Θετικών και Εφαρμοσμένων Επιστημών / Faculty of Pure and Applied SciencesΤμήμα Πληροφορικής / Department of Computer Science
dc.type.uhtypeConference Objecten
dc.description.notes<p>Sponsors: IEEE Comput. Soc. Technical Committee on Distributed Processingen
dc.description.notesAkamai Technologies, Inc.en
dc.description.notesInternational Research Institute on Autonomic Network Computingen
dc.description.notesConference code: 73523en
dc.description.notesCited By :2</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