{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T13:18:28Z","timestamp":1774012708555,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,1,8]],"date-time":"2009-01-08T00:00:00Z","timestamp":1231372800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10009-008-0097-7","type":"journal-article","created":{"date-parts":[[2009,1,7]],"date-time":"2009-01-07T07:56:51Z","timestamp":1231315011000},"page":"153-171","source":"Crossref","is-referenced-by-count":13,"title":["Automated implementation of complex distributed algorithms specified in the IOA language"],"prefix":"10.1007","volume":"11","author":[{"given":"Chryssis","family":"Georgiou","sequence":"first","affiliation":[]},{"given":"Nancy","family":"Lynch","sequence":"additional","affiliation":[]},{"given":"Panayiotis","family":"Mavrommatis","sequence":"additional","affiliation":[]},{"given":"Joshua A.","family":"Tauber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,1,8]]},"reference":[{"key":"97_CR1","unstructured":"Georgiou, C., Lynch, N., Mavrommatis, P., Tauber, J.A.: Automated implementation of complex distributed algorithms specified in the IOA language. In: Proceedings of 18th International Conference on Parallel and Distributed Computing Systems (PDCS 2005), pp. 128\u2013134 (2005)"},{"key":"97_CR2","unstructured":"Garland, S., Lynch, N., Tauber, J., Vaziri, M.: IOA user guide and reference manual. Technical Report MIT\/LCS\/TR-961, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, July 2004. http:\/\/theory.lcs.mit.edu\/tds\/ioa\/manual.ps ."},{"key":"97_CR3","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 137\u2013151, Vancouver, British Columbia, Canada (1987)","DOI":"10.1145\/41840.41852"},{"key":"97_CR4","unstructured":"Lynch N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI-Quarterly. 2 (3), 219\u2013246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands. Technical Memo MIT\/LCS\/TM-373, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, November 1988"},{"key":"97_CR5","unstructured":"Chefter, A.E.: A simulator for the IOA language. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (1998)"},{"key":"97_CR6","unstructured":"Dean, L.G.: Improved simulation of Input\/Output automata. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2001)"},{"key":"97_CR7","unstructured":"K\u0131rl\u0131 Kaynar, D., Chefter, A., Dean, L., Garland, S., Lynch, N., Ne Win, T., Ram\u0131rez-Robredo, A.: The IOA simulator. Technical Report MIT-LCS-TR-843, MIT Laboratory for Computer Science, Cambridge, MA, July 2002"},{"key":"97_CR8","unstructured":"Antonio Ram\u0131rez-Robredo, J.: Paired simulation of I\/O automata. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2000)"},{"key":"97_CR9","unstructured":"Solovey, E.: Simulation of composite I\/O automata. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2003)"},{"key":"97_CR10","unstructured":"Tsai, M.J.: Code generation for the IOA language. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2002)"},{"key":"97_CR11","unstructured":"Ne Win, T.: Theorem-proving distributed algorithms with dynamic analysis. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2003)"},{"key":"97_CR12","unstructured":"Bogdanov, A.: Formal verification of simulations between I\/O automata. Master\u2019s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2001)"},{"key":"97_CR13","unstructured":"Garland, S.J., Lynch, N.A.: The IOA language and toolset: support for designing, analyzing, and building distributed systems. Technical Report MIT\/LCS\/TR-762, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, August 1998. http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/IOA-TR-762.ps"},{"key":"97_CR14","unstructured":"Tauber, J.A.: Verifiable Compilation of I\/O Automata without Global Synchronization. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA (2004)"},{"key":"97_CR15","doi-asserted-by":"crossref","unstructured":"Tauber, J.A., Lynch, N.A., Tsai, M.J.: Compiling IOA without global synchronization. In: Proceedings of the 3rd IEEE International Symposium on Network Computing and Applications (IEEE NCA04), pp. 121\u2013130. Cambridge, MA (2004)","DOI":"10.1109\/NCA.2004.1347769"},{"issue":"5","key":"97_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E. Chang","year":"1979","unstructured":"Chang E., Roberts R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979)","journal-title":"Commun. ACM"},{"issue":"4","key":"97_CR17","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1109\/TSE.1982.235573","volume":"SE-8","author":"E.J.H. Chang","year":"1982","unstructured":"Chang E.J.H.: Echo algorithms: depth parallel operations on general graphs. IEEE Trans. Softw. Eng. SE-8(4), 391\u2013401 (1982)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"97_CR18","unstructured":"Le Lann, G.: Distributed systems\u2014towards a formal approach. In: Gilchrist, B. (ed.) Information Processing 77 (Toronto, August 1977). Proceedings of IFIP Congress, vol. 7, pp. 155\u2013160. North-Holland Publishing Co., Amsterdam (1977)"},{"key":"97_CR19","doi-asserted-by":"crossref","unstructured":"Segall, A.: Distributed network protocols. IEEE Trans. Inf. Theory IT-29(1), 23\u201335 (1983)","DOI":"10.1109\/TIT.1983.1056620"},{"key":"97_CR20","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch N.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Mateo, CA (1996)"},{"key":"97_CR21","doi-asserted-by":"crossref","unstructured":"Humblet, P.A., Gallager, R.G., Spira, P.M.: A distributed algorithm for minimum-weight spanning trees. In: ACM Transactions on Programming Languages and Systems, vol. 5(1), pp. 66\u201377 (1983)","DOI":"10.1145\/357195.357200"},{"key":"97_CR22","doi-asserted-by":"crossref","unstructured":"Lampoft, L., Welch, J., Lynch, N.: A lattice-structured proof of a minimum spanning tree algorithm. In: Proceedings of 7th ACM Symposium on Principles of Distributed Computing, pp. 28\u201343 (1988)","DOI":"10.1145\/62546.62552"},{"key":"97_CR23","unstructured":"Message Passing Interface Forum. MPI: A message-passing interface standard. Int. J. Supercomput. Appl. 8(3\u20134), 1994"},{"issue":"4","key":"97_CR24","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01784720","volume":"6","author":"K.J. Goldman","year":"1991","unstructured":"Goldman K.J.: Highly concurrent logically synchronous multicast. Distrib. Comput. 6(4), 189\u2013207 (1991)","journal-title":"Distrib. Comput."},{"issue":"9","key":"97_CR25","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1109\/32.464547","volume":"21","author":"K.J. Goldman","year":"1995","unstructured":"Goldman K.J., Swaminathan B., Paul McCartney T., Anderson M.D., Sethuraman R.: The Programmers\u2019 Playground: I\/O abstraction for user-configurable distributed applications. IEEE Trans. Softw. Eng. 21(9), 735\u2013746 (1995)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"97_CR26","doi-asserted-by":"crossref","unstructured":"Cheiner, O., Shvartsman, A.: Implementing an eventually-serializable data service as a distributed system building block. In: Mavronicolas, M., Merritt, M., Shavit, N. (eds.) Networks in Distributed Computing. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 45, pp. 43\u201372. American Mathematical Society, Providence, RI (1999)","DOI":"10.1090\/dimacs\/045\/03"},{"key":"97_CR27","doi-asserted-by":"crossref","unstructured":"Fekete, A., Gupta, D., Luchangco, V., Lynch, N., Shvartsman, A.: Eventually-serializable data services. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 300\u2013309, Philadelphia, PA (1996)","DOI":"10.1145\/248052.248113"},{"key":"97_CR28","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare C.A.R.: Communicating Sequential Processes. Prentice-Hall International, UK (1985)"},{"key":"97_CR29","unstructured":"INMOS Ltd: occam Programming Manual (1984)"},{"key":"97_CR30","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner R.: Communication and Concurrency. Prentice-Hall International, UK (1989)"},{"key":"97_CR31","doi-asserted-by":"crossref","unstructured":"Vaandrager, F.W.: On the relationship between process algebra and input\/output automata. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS 1991), pp. 387\u2013398 (1991)","DOI":"10.1109\/LICS.1991.151662"},{"key":"97_CR32","doi-asserted-by":"crossref","unstructured":"Gelastou, M., Georgiou, C., Philippou, A.: On the application of formal methods for specifying and verifying distributed protocols. In: Proceedings of the 7th IEEE International Symposium on Network Computing and Applications (NCA 2008), pp. 195\u2013204 (2008)","DOI":"10.1109\/NCA.2008.24"},{"key":"97_CR33","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Parrow, J., Steffen ,B.U.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM TOPLAS 15(1), 1993 (1993)","DOI":"10.1145\/151646.151648"},{"key":"97_CR34","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Gada, J.N., Lewis, P.M., Smolka, S.A., Sokolsky, O., Zhang, S.: The Concurrency Factory\u2014practical tools for specification, simulation, verification and implementation of concurrent systems. In: Specification of Parallel Algorithms. DIMACS Workshop, pp. 75\u201389. American Mathematical Society, Providence, RI (1994)","DOI":"10.1090\/dimacs\/018\/06"},{"key":"97_CR35","unstructured":"Baker, M., Carpenter, B., Ko, S.H., Li, X.: mpiJava: A Java interface to MPI. First UK Workshop on Java for High Performance Network Computing, Europar (1998, presented)"},{"key":"97_CR36","unstructured":"Tauber, J.A., Garland, S.J.: Definition and expansion of composite automata in IOA. Technical Report MIT\/LCS\/TR-959, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, July 2004. http:\/\/theory.lcs.mit.edu\/tds\/papers\/Tauber\/MIT-LCS-TR-959.pdf"},{"key":"97_CR37","doi-asserted-by":"crossref","unstructured":"Georgiou, C., Musial, P.M., Shvartsman, A.A., Sonderegger, E.L.: An abstract channel specification and an algorithm implementing it using java sockets. In: Proceedings of the 7th IEEE International Symposium on Network Computing and Applications (NCA 2008), pp. 211\u2013219 (2008)","DOI":"10.1109\/NCA.2008.12"},{"key":"97_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01794-0","volume-title":"The Theory of Timed I\/O Automata","author":"D.K. Kaynar","year":"2006","unstructured":"Kaynar D.K., Lynch N., Segala R., Vaandrager F.: The Theory of Timed I\/O Automata. Morgan & Claypool Publishers, San Francisco (2006)"},{"key":"97_CR39","doi-asserted-by":"crossref","unstructured":"Lynch, N., Michel, L., Shvartsman, A.: Tempo: A toolkit for the timed input\/output automata formalism. In: Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks, and Systems (SIMUTools 2008)\u2014Industrial Track: Simulation Works (2008)","DOI":"10.4108\/ICST.SIMUTOOLS2008.3105"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0097-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-008-0097-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0097-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T20:35:35Z","timestamp":1738874135000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-008-0097-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,8]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["97"],"URL":"https:\/\/doi.org\/10.1007\/s10009-008-0097-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1,8]]}}}