dc.contributor.author | Georgiou, Chryssis | en |
dc.contributor.author | Lynch, N. | en |
dc.contributor.author | Mavrommatis, Panayiotis | en |
dc.contributor.author | Tauber, J. A. | en |
dc.creator | Georgiou, Chryssis | en |
dc.creator | Lynch, N. | en |
dc.creator | Mavrommatis, Panayiotis | en |
dc.creator | Tauber, J. A. | en |
dc.date.accessioned | 2019-11-13T10:40:10Z | |
dc.date.available | 2019-11-13T10:40:10Z | |
dc.date.issued | 2009 | |
dc.identifier.issn | 1433-2779 | |
dc.identifier.uri | http://gnosis.library.ucy.ac.cy/handle/7/53989 | |
dc.description.abstract | IOA is a formal language for describing Input/Output automata that serves both as a formal specification language and as a programming language (Garland et al. in http://theory.lcs.mit.edu/tds/ioa/manual.ps, 2004). The IOA compiler automatically translates IOA specifications into Java code that runs on a set of workstations communicating via the Message Passing Interface. This paper describes the process of compiling IOA specifications and our experiences running several distributed algorithms, ranging from simple ones such as the Le Lann, Chang and Roberts (LCR) leader election in a ring algorithm to that of Gallager, Humblet and Spira (GHS) for minimum-weight spanning tree formation in an arbitrary graph (Humblet et al. in ACM Trans Program Lang Syst 5(1):66-77, 1983). Our IOA code for all the algorithms is derived from their Input/Output automaton descriptions that have already been formally proved correct. The successful implementation of these algorithms is significant for two reasons: (a) it is an indication of the capabilities of the IOA compiler and of its advanced state of development, and (b) to the best of our knowledge, these are the first complex, distributed algorithms implemented in an automated way that have been formally and rigorously proved correct. Thus, this work shows that it is possible to formally specify, prove correct, and implement complex distributed algorithms using a common formal methodology. © Springer-Verlag 2009. | en |
dc.source | International Journal on Software Tools for Technology Transfer | en |
dc.source.uri | https://www.scopus.com/inward/record.uri?eid=2-s2.0-60849135690&doi=10.1007%2fs10009-008-0097-7&partnerID=40&md5=47cf5ba2c19fc318ebf5ec52c7fcd6eb | |
dc.subject | Specifications | en |
dc.subject | Parallel algorithms | en |
dc.subject | Linguistics | en |
dc.subject | Automata theory | en |
dc.subject | Translation (languages) | en |
dc.subject | Automation | en |
dc.subject | Robots | en |
dc.subject | Trees (mathematics) | en |
dc.subject | Distributed algorithms | en |
dc.subject | Message passing | en |
dc.subject | Program compilers | en |
dc.subject | Network components | en |
dc.subject | Java codes | en |
dc.subject | Arbitrary graphs | en |
dc.subject | Automated code generator | en |
dc.subject | Formal languages | en |
dc.subject | Formal methods | en |
dc.subject | Formal specification languages | en |
dc.subject | Input/Output automata | en |
dc.subject | IOA Toolkit | en |
dc.subject | Leader elections | en |
dc.subject | Message passing interfaces | en |
dc.subject | Programming languages | en |
dc.subject | Spanning trees | en |
dc.subject | Specification languages | en |
dc.subject | Verifiable distributed code | en |
dc.title | Automated implementation of complex distributed algorithms specified in the IOA language | en |
dc.type | info:eu-repo/semantics/article | |
dc.identifier.doi | 10.1007/s10009-008-0097-7 | |
dc.description.volume | 11 | |
dc.description.issue | 2 | |
dc.description.startingpage | 153 | |
dc.description.endingpage | 171 | |
dc.author.faculty | 002 Σχολή Θετικών και Εφαρμοσμένων Επιστημών / Faculty of Pure and Applied Sciences | |
dc.author.department | Τμήμα Πληροφορικής / Department of Computer Science | |
dc.type.uhtype | Article | en |
dc.description.notes | <p>Cited By :10</p> | en |
dc.source.abbreviation | Int.J.Softw.Tools Technol.Trans. | en |
dc.contributor.orcid | Georgiou, Chryssis [0000-0003-4360-0260] | |
dc.gnosis.orcid | 0000-0003-4360-0260 | |