Automated implementation of complex distributed algorithms specified in the IOA language
Date
2009ISSN
1433-2779Source
International Journal on Software Tools for Technology TransferVolume
11Issue
2Pages
153-171Google Scholar check
Keyword(s):
Metadata
Show full item recordAbstract
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.
Collections
Cite as
Related items
Showing items related by title, author, creator and subject.
-
Article
Russian language for business communication. New book for teaching Russian as a foreign language
Tairova, Marina (2009)
-
Conference Object
Η διδασκαλία της Ελληνικής γλώσσας ως δεύτερης γλώσσας: περιπτωσιακή μελέτη σε γυναίκες Ρομα στον οικισμό στα Πολεμίδια [Greek Language as a Second Language (L2). Case study in teaching Greek to Roma women at Polemidia area, Limassol]
Πελεκανή, Χρύσω (Ευρωπαϊκό Πανεπιστήμιο Κύπρου, 2014)Τα τελευταία δέκα χρόνια παρατηρείται μια έντονη κινητικότητα από το Υπουργείο Παιδείας και Πολιτισμού και άλλων κυβερνητικών ή μη οργανισμών, φορέων και ιδρυμάτων γύρω από θέμα των Ρομά και την ομαλή ένταξή τους στην ...
-
Conference Object
Classroom Activities in Turkish Communicative Language Teaching (TCLT) : Theory and Practice (AEP-Language Center, UCY) [Δραστηριότητες στην Τάξη για την Επικοινωνιακή Διδασκαλία της Τουρκικής Γλώσσας: Θεωρία και Πρακτική]
Pelekani, Chryso; Georgiou, Eleni; Veysioğlu, Yasemin (Language Centre, University of Cyprus, 2016)The present study aims to introduce a number of communicative activities/tasks (group work and pair work, drama, improvisation, role-playing, simulation, problem solving, communication games) used in Turkish Language classes ...