{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:41:32Z","timestamp":1725860492857},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415789"},{"type":"electronic","value":"9783319415796"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41579-6_15","type":"book-chapter","created":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T02:44:48Z","timestamp":1466995488000},"page":"186-202","source":"Crossref","is-referenced-by-count":0,"title":["Modeling Actor Systems Using Dynamic I\/O Automata"],"prefix":"10.1007","author":[{"given":"Ilham W.","family":"Kurnia","sequence":"first","affiliation":[]},{"given":"Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,28]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: FSTTCS, pp. 653\u2013665 (2014)","DOI":"10.1007\/978-3-319-26850-7_2"},{"key":"15_CR2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: A Model of Concurrent Computation in Distributed Systems","author":"G Agha","year":"1986","unstructured":"Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/978-3-540-39993-3_4","volume-title":"From Object-Orientation to Formal Methods","author":"G Agha","year":"2004","unstructured":"Agha, G., Thati, P.: An algebraic theory of actors and its application to a simple object-based language. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 26\u201357. Springer, Heidelberg (2004)"},{"issue":"12","key":"15_CR4","doi-asserted-by":"crossref","first-page":"1289","DOI":"10.1016\/j.scico.2010.08.003","volume":"77","author":"W Ahrendt","year":"2012","unstructured":"Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289\u20131309 (2012)","journal-title":"Sci. Comput. Program."},{"key":"15_CR5","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(83)90066-X","volume":"28","author":"KR Apt","year":"1984","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey part II: nondeterminism. Theor. Comput. Sci. 28, 83\u2013109 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-44685-0_10","volume-title":"CONCUR 2001 - Concurrency Theory","author":"PC Attie","year":"2001","unstructured":"Attie, P.C., Lynch, N.A.: Dynamic Input\/Output automata: a formal model for dynamic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 137\u2013151. Springer, Heidelberg (2001)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Attie, P.C., Lynch, N.: Dynamic Input\/Output automata: a formal and compositional model for dynamic systems. Inf. Comput. (2015) (To appear)","DOI":"10.1016\/j.ic.2016.03.008"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/978-3-642-37064-9_17","volume-title":"Language and Automata Theory and Applications","author":"B Bollig","year":"2013","unstructured":"Bollig, B., Cyriac, A., H\u00e9lou\u00ebt, L., Kara, A., Schwentick, T.: Dynamic communicating automata and branching high-level MSCs. In: Dediu, A.-H., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 177\u2013189. Springer, Heidelberg (2013)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/978-3-642-13182-0_5","volume-title":"Computer Science \u2013 Theory and Applications","author":"B Bollig","year":"2010","unstructured":"Bollig, B., H\u00e9lou\u00ebt, L.: Realizability of dynamic MSC languages. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 48\u201359. Springer, Heidelberg (2010)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-642-40213-5_8","volume-title":"Fundamentals of Software Engineering","author":"A Boudjadar","year":"2013","unstructured":"Boudjadar, A., Vaandrager, F., Bodeveix, J.-P., Filali, M.: Extending UPPAAL for the modeling and verification of dynamic real-time systems. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 111\u2013132. Springer, Heidelberg (2013)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/3-540-49213-5_7","volume-title":"Compositionality: The Significant Difference","author":"M Dam","year":"1998","unstructured":"Dam, M., Fredlund, L., Gurov, D.: Toward parametric verification of open distributed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 150\u2013185. Springer, Heidelberg (1998)"},{"issue":"3","key":"15_CR12","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.jlap.2012.01.003","volume":"81","author":"CC Din","year":"2012","unstructured":"Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Log. Algebr. Program. 81(3), 227\u2013256 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Din, C.C., Owe, O.: Compositional and sound reasoning about active objects with shared futures. Research report 437 (2014)","DOI":"10.1007\/s00165-014-0322-y"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/978-3-642-38856-9_24","volume-title":"Static Analysis","author":"E D\u2019Osualdo","year":"2013","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of erlang-style concurrency. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 454\u2013476. Springer, Heidelberg (2013)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: SwSTE, pp. 141\u2013150 (2005)","DOI":"10.1109\/SWSTE.2005.24"},{"issue":"3","key":"15_CR16","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1017\/S0960129599002765","volume":"9","author":"CHC Duarte","year":"1999","unstructured":"Duarte, C.H.C.: Proof-theoretic foundations for the design of actor systems. Math. Struct. Comput. Sci. 9(3), 227\u2013252 (1999)","journal-title":"Math. Struct. Comput. Sci."},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1007\/978-3-642-23217-6_27","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"J Fisher","year":"2011","unstructured":"Fisher, J., Henzinger, T.A., Nickovic, D., Piterman, N., Singh, A.V., Vardi, M.Y.: Dynamic reactive modules. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 404\u2013418. Springer, Heidelberg (2011)"},{"key":"15_CR18","volume-title":"FMOODS","author":"M Gaspari","year":"1999","unstructured":"Gaspari, M., Zavattaro, G.: An algebra of actors. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) FMOODS. Springer, New York (1999)"},{"issue":"2\u20133","key":"15_CR19","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1016\/j.tcs.2008.09.019","volume":"410","author":"P Haller","year":"2009","unstructured":"Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2\u20133), 202\u2013220 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR20","unstructured":"International Telecommunication Union - Telecommunication Standardization. Open distributed processing - reference models parts 1\u20134. Technical report, ISO\/IEC (1995)"},{"key":"15_CR21","unstructured":"International Telecommunication Union - Telecommunication Standardization. Recommendation Z.120: Message Sequence Chart (MSC). Technical report, ISO\/IEC (2011)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Jaghoori, M.M., Chothia, T.: Timed automata semantics for analyzing Creol. In: FOCLASA, pp. 108\u2013122 (2010)","DOI":"10.4204\/EPTCS.30.8"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011)"},{"key":"15_CR24","unstructured":"Kurnia, I.W.: An automata-theoretic approach to open actor system verification. Ph.D. thesis, University of Kaiserslautern, January 2015"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Kurnia, I.W., Poetzsch-Heffter, A.: A relational trace logic for simple hierarchical actor-based component systems. In: AGERE! 2012, pp. 47\u201358. ACM (2012)","DOI":"10.1145\/2414639.2414647"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-642-40615-7_3","volume-title":"Formal Methods for Components and Objects","author":"IW Kurnia","year":"2013","unstructured":"Kurnia, I.W., Poetzsch-Heffter, A.: Verification of open concurrent object systems. In: Giachino, E., H\u00e4hnle, R., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 7866, pp. 83\u2013118. Springer, Heidelberg (2013)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Lamport, L.: What good is temporal logic? In: IFIP Congress, pp. 657\u2013668 (1983)","DOI":"10.1145\/2402.322398"},{"key":"15_CR28","unstructured":"Leo, J.: Dynamic process creation in a static model. Master\u2019s thesis, MIT (1990)"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Lynch, N., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137\u2013151 (1987)","DOI":"10.1145\/41840.41852"},{"issue":"4","key":"15_CR30","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Mani Chandy, K.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Software Eng."},{"key":"15_CR31","first-page":"170","volume":"10","author":"U Montanari","year":"1997","unstructured":"Montanari, U., Pistore, M.: Ugo Montanari and Marco Pistore. ENTCS 10, 170\u2013188 (1997)","journal-title":"ENTCS"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11419822_1","volume-title":"Formal Methods for Mobile Computing","author":"U Montanari","year":"2005","unstructured":"Montanari, U., Pistore, M.: History-dependent automata: an introduction. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol. 3465, pp. 1\u201328. Springer, Heidelberg (2005)"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","first-page":"101","volume-title":"Types for Proofs and Programs","author":"T Nipkow","year":"1994","unstructured":"Nipkow, T., Slind, K.: I\/O automata in Isabelle\/HOL. In: Dybjer, P., Nordstr\u00f6m, B., Smith, J. (eds.) TYPES. LNCS, vol. 996, pp. 101\u2013119. Springer, Heidelberg (1994)"},{"issue":"3","key":"15_CR34","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1145\/44501.44504","volume":"10","author":"E-R Olderog","year":"1988","unstructured":"Olderog, E.-R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM TOPLAS 10(3), 420\u2013455 (1988)","journal-title":"ACM TOPLAS"},{"key":"15_CR35","unstructured":"OSGi core release 5 (2012). http:\/\/www.osgi.org"},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/3-540-45397-0_18","volume-title":"Concurrent Object-Oriented Programming and Petri Nets","author":"S Schacht","year":"2001","unstructured":"Schacht, S.: Formal reasoning about actor programs using temporal logic. In: Agha, G., De Cindio, F., Rozenberg, G. (eds.) APN 2001. LNCS, vol. 2001, pp. 445\u2013460. Springer, Heidelberg (2001)"},{"key":"15_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/11767954_18","volume-title":"Coordination Models and Languages","author":"M Sirjani","year":"2006","unstructured":"Sirjani, M., Jaghoori, M.M., Baier, C., Arbab, F.: Compositional semantics of an actor-based language using constraint automata. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 281\u2013297. Springer, Heidelberg (2006)"},{"issue":"4","key":"15_CR38","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1023\/A:1022934504959","volume":"15","author":"S Smith","year":"2002","unstructured":"Smith, S., Talcott, C.L.: Specification diagrams for actor systems. High.-Order Symb. Comput. 15(4), 301\u2013348 (2002)","journal-title":"High.-Order Symb. Comput."},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/978-3-540-27815-3_39","volume-title":"Algebraic Methodology and Software Technology","author":"P Thati","year":"2004","unstructured":"Thati, P., Talcott, C., Agha, G.: Techniques for executing and reasoning about specification diagrams. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 521\u2013536. Springer, Heidelberg (2004)"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/978-3-642-27940-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Zufferey","year":"2012","unstructured":"Zufferey, D., Wies, T., Henzinger, T.A.: Ideal abstractions for well-structured transition systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 445\u2013460. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41579-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T23:42:33Z","timestamp":1600818153000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41579-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415789","9783319415796"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41579-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}