{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T16:21:06Z","timestamp":1747153266041,"version":"3.40.5"},"publisher-location":"Cham","reference-count":82,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031353604"},{"type":"electronic","value":"9783031353611"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-35361-1_5","type":"book-chapter","created":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T14:04:07Z","timestamp":1686751447000},"page":"93-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Shelley: A Framework for\u00a0Model Checking Call Ordering on\u00a0Hierarchical Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6835-3097","authenticated-orcid":false,"given":"Carlos M\u00e3o","family":"de Ferro","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3209-9258","authenticated-orcid":false,"given":"Tiago","family":"Cogumbreiro","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2379-7257","authenticated-orcid":false,"given":"Francisco","family":"Martins","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,15]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)","edition":"1"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Aldrich, J., Sunshine, J., Saini, D., Sparks, Z.: Typestate-oriented programming. In: OOPSLA, New York, NY, USA, pp. 1015\u20131022. ACM (2009). https:\/\/doi.org\/10.1145\/1639950.1640073","DOI":"10.1145\/1639950.1640073"},{"issue":"3","key":"5_CR3","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing ltl semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-22655-7_2","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"NE Beckman","year":"2011","unstructured":"Beckman, N.E., Kim, D., Aldrich, J.: An empirical study of object protocols in the wild. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 2\u201326. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22655-7_2"},{"issue":"2","key":"5_CR5","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A Benveniste","year":"1991","unstructured":"Benveniste, A., Le Guernic, P., Jacquemot, C.: Synchronous Programming with Events and Relations: the SIGNAL Language and Its Semantics. Sci. Comput. Program. 16(2), 103\u2013149 (1991). https:\/\/doi.org\/10.1016\/0167-6423(91)90001-E","journal-title":"Sci. Comput. Program."},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/3-540-15670-4_19","volume-title":"Seminar on Concurrency","author":"G Berry","year":"1985","unstructured":"Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 389\u2013448. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15670-4_19"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: Gabriel, R.P., Bacon, D.F., Lopes, C.V., Jr., G.L.S. (eds.) OOPSLA. pp. 301\u2013320. ACM (2007). https:\/\/doi.org\/10.1145\/1297027.1297050","DOI":"10.1145\/1297027.1297050"},{"issue":"11","key":"5_CR9","doi-asserted-by":"publisher","first-page":"1801","DOI":"10.1002\/spe.2495","volume":"47","author":"S Bliudze","year":"2017","unstructured":"Bliudze, S., Mavridou, A., Szymanek, R., Zolotukhina, A.: Exogenous coordination of concurrent software components with Javabip. Softw. Pract. Exp. 47(11), 1801\u20131836 (2017). https:\/\/doi.org\/10.1002\/spe.2495","journal-title":"Softw. Pract. Exp."},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-030-76384-8_4","volume-title":"NASA Formal Methods","author":"H Bourbouh","year":"2021","unstructured":"Bourbouh, H., et al.: Integrating formal verification and assurance: an inspection rover case study. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 53\u201371. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_4"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-030-64437-6_6","volume-title":"Programming Languages and Systems","author":"M Bravetti","year":"2020","unstructured":"Bravetti, M., et al.: Behavioural types for memory and method safety in a core object-oriented language. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 105\u2013124. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_6"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"issue":"1","key":"5_CR14","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/32.120312","volume":"18","author":"D Coleman","year":"1992","unstructured":"Coleman, D., Hayes, F., Bear, S.: Introducing Objectcharts or How to Use Statecharts in Object-Oriented Design. IEEE Trans. Software Eng. 18(1), 9\u201318 (1992). https:\/\/doi.org\/10.1109\/32.120312","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-18941-3_4","volume-title":"Formal Methods for Multicore Programming","author":"M Coppo","year":"2015","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146\u2013178. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-18941-3_4"},{"key":"5_CR16","doi-asserted-by":"publisher","DOI":"10.1155\/2013\/171647","author":"Z Dai","year":"2013","unstructured":"Dai, Z., Mao, X., Lei, Y., Qi, Y., Wang, R., Gu, B.: Compositional mining of multiple object API protocols through state abstraction. Sci. World J. (2013). https:\/\/doi.org\/10.1155\/2013\/171647","journal-title":"Sci. World J."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: AAAI, pp. 1027\u20131033. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"5_CR18","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860. AAAI Press (2013)"},{"key":"5_CR19","unstructured":"DeLIne, R., Fahndrich, M.: The fugue protocol checker: Is your software baroque? Tech. report MSR-TR-2004-07, January 2004. https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-fugue-protocol-checker-is-your-software-baroque\/"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-28869-2_10","volume-title":"Programming Languages and Systems","author":"P-M Deni\u00e9lou","year":"2012","unstructured":"Deni\u00e9lou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194\u2013213. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_10"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Desai, A., Phanishayee, A., Qadeer, S., Seshia, S.A.: Compositional programming and testing of dynamic distributed systems. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276529","DOI":"10.1145\/3276529"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Desai, A., et al.: P: Safe Asynchronous Event-driven Programming. In: PLDI, pp. 321\u2013332. ACM (2013)","DOI":"10.1145\/2499370.2462184"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/11785477_20","volume-title":"ECOOP 2006 \u2013 Object-Oriented Programming","author":"M Dezani-Ciancaglini","year":"2006","unstructured":"Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session types for object-oriented languages. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 328\u2013352. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11785477_20"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Duarte, J., Ravara, A.: Retrofitting typestates into rust. In: Vasconcellos, C.D., Roggia, K.G., Bousfield, P., Collereii, V., Fernandes, J.P., Pereira, M. (eds.) SBLP, pp. 83\u201391. ACM (2021). https:\/\/doi.org\/10.1145\/3475061.3475082","DOI":"10.1145\/3475061.3475082"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Dutle, A., et al.: From requirements to autonomous flight: an overview of the monitoring ICAROUS project. In: Luckcuck, M., Farrell, M. (eds.) FMAS. EPTCS, vol. 329, pp. 23\u201330 (2020). https:\/\/doi.org\/10.4204\/EPTCS.329.3","DOI":"10.4204\/EPTCS.329.3"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"de Ferro, C.M., Cogumbreiro, T., Martins, F.: Shelley: a framework for model checking call ordering on hierarchical systems, May 2023. https:\/\/doi.org\/10.5281\/zenodo.7884206","DOI":"10.5281\/zenodo.7884206"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L., Ghassabani, E.: The JKind model checker. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 20\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Garcia, R., Tanter, E., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36(4) (2014). https:\/\/doi.org\/10.1145\/2629609","DOI":"10.1145\/2629609"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Gesbert, N., Ravara, A., Vasconcelos, V.T.: Modular session types for objects. Log. Methods Comput. Sci. 11(4) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(4:12)2015","DOI":"10.2168\/LMCS-11(4:12)2015"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Vasconcelos, V.T., Ravara, A., Gesbert, N., Caldeira, A.Z.: Modular session types for distributed object-oriented programming. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 299\u2013312. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706335","DOI":"10.1145\/1706299.1706335"},{"key":"5_CR31","unstructured":"George, D.: MicroPython (2022). https:\/\/micropython.org"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Georges, A., Buytaert, D., Eeckhout, L.: Statistically rigorous java performance evaluation. In: OOPSLA, pp. 57\u201376. ACM (2007)","DOI":"10.1145\/1297105.1297033"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-00593-0_7","volume-title":"Fundamental Approaches to Software Engineering","author":"D Giannakopoulou","year":"2009","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Interface generation and compositional verification in JavaPathfinder. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 94\u2013108. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_7"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Gordon, C.S.: Polymorphic iterable sequential effect systems. ACM Trans. Program. Lang. Syst. 43(1) (2021). https:\/\/doi.org\/10.1145\/3450272","DOI":"10.1145\/3450272"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-030-40914-2_2","volume-title":"Formal Aspects of Component Software","author":"JF Groote","year":"2020","unstructured":"Groote, J.F., Keiren, J.J.A., Luttik, B., de Vink, E.P., Willemse, T.A.C.: Modelling and analysing software in mCRL2. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 25\u201348. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-40914-2_2"},{"issue":"9","key":"5_CR36","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"issue":"3","key":"5_CR37","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987). https:\/\/doi.org\/10.1016\/0167-6423(87)90035-9","journal-title":"Sci. Comput. Program."},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"CONCUR 2001 \u2014 Concurrency Theory","author":"J Hatcliff","year":"2001","unstructured":"Hatcliff, J., Dwyer, M.: Using the Bandera tool set to model-check properties of concurrent Java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 39\u201358. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44685-0_5"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: ESEC\/FSE. p. 31\u201340. ACM (2005). https:\/\/doi.org\/10.1145\/1081706.1081713","DOI":"10.1145\/1081706.1081713"},{"issue":"5","key":"5_CR40","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122\u2013138. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0053567"},{"issue":"1","key":"5_CR42","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/2827695","volume":"63","author":"K Honda","year":"2016","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1-9:67 (2016). https:\/\/doi.org\/10.1145\/2827695","journal-title":"J. ACM"},{"key":"5_CR43","unstructured":"Jacklin, S.A.: Survey of verification and validation techniques for small satellite software development. Technical report (2015)"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Jakobsen, M., Ravier, A., Dardha, O.: Papaya: global typestate analysis of aliased objects. In: Veltri, N., Benton, N., Ghilezan, S. (eds.) PPDP, pp. 19:1\u201319:13. ACM (2021). https:\/\/doi.org\/10.1145\/3479394.3479414","DOI":"10.1145\/3479394.3479414"},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"Katis, A., Mavridou, A., Giannakopoulou, D., Pressburger, T., Schumann, J.: Capture, analyze, diagnose: Realizability checking of requirements in FRET. In: Shoham, S., Vizel, Y. (eds.) CAV. LNCS, vol. 13372, pp. 490\u2013504. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_24","DOI":"10.1007\/978-3-031-13188-2_24"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Kofron, J.: Checking software component behavior using behavior protocols and spin. In: Proceedings of SAC, pp. 1513\u20131517. ACM (2007). https:\/\/doi.org\/10.1145\/1244002.1244326","DOI":"10.1145\/1244002.1244326"},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"Koskinen, E., Terauchi, T.: Local temporal reasoning. In: CSL-LICS. ACM (2014). https:\/\/doi.org\/10.1145\/2603088.2603138","DOI":"10.1145\/2603088.2603138"},{"key":"5_CR48","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.scico.2017.10.006","volume":"155","author":"D Kouzapas","year":"2018","unstructured":"Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with mungo and stmungo: a session type toolchain for java. Sci. Comput. Program. 155, 52\u201375 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.10.006","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"5_CR49","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/2736348","volume":"58","author":"L Lamport","year":"2015","unstructured":"Lamport, L.: Who builds a house without drawing blueprints? Commun. ACM 58(4), 38\u201341 (2015). https:\/\/doi.org\/10.1145\/2736348","journal-title":"Commun. ACM"},{"key":"5_CR50","doi-asserted-by":"publisher","unstructured":"Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: POPL, pp. 221\u2013232. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676964","DOI":"10.1145\/2676726.2676964"},{"key":"5_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-25540-4_6","volume-title":"Computer Aided Verification","author":"J Lange","year":"2019","unstructured":"Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 97\u2013117. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_6"},{"issue":"1\u20132","key":"5_CR52","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/s100090050010","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-319-40648-0_28","volume-title":"NASA Formal Methods","author":"J Liu","year":"2016","unstructured":"Liu, J., Backes, J.D., Cofer, D., Gacek, A.: From design contracts to component requirements verification. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 373\u2013387. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_28"},{"issue":"1","key":"5_CR54","first-page":"22","volume":"6","author":"M Mach","year":"2005","unstructured":"Mach, M., Pl\u00e1sil, F., Kofron, J.: Behavior protocol verification: fighting state explosion. Int. J. Comput. Inf. Sci. 6(1), 22\u201330 (2005)","journal-title":"Int. J. Comput. Inf. Sci."},{"key":"5_CR55","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, 2 edn. (2006)"},{"key":"5_CR56","unstructured":"Mavridou, A., Bourbouh, H., Garoche, P., Giannakopoulou, D., Pressburger, T., Schumann, J.: Bridging the gap between requirements and simulink model analysis. In: Sabetzadeh, M., et al. (eds.) REFSQ. CEUR Workshop Proceedings, vol. 2584. CEUR-WS.org (2020)"},{"key":"5_CR57","doi-asserted-by":"publisher","unstructured":"Mavridou, A., et al.: The ten lockheed martin cyber-physical challenges: formalized, analyzed, and explained. In: Breaux, T.D., Zisman, A., Fricker, S., Glinz, M. (eds.) RE, pp. 300\u2013310. IEEE (2020). https:\/\/doi.org\/10.1109\/RE48521.2020.00040","DOI":"10.1109\/RE48521.2020.00040"},{"key":"5_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-030-90870-6_27","volume-title":"Formal Methods","author":"A Mavridou","year":"2021","unstructured":"Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 503\u2013523. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27"},{"key":"5_CR59","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Verisolid: Correct-by-design smart contracts for ethereum. CoRR abs\/1901.01292 (2019). http:\/\/arxiv.org\/abs\/1901.01292"},{"key":"5_CR60","doi-asserted-by":"publisher","unstructured":"Moln\u00e1r, V., Graics, B., V\u00f6r\u00f6s, A., Majzik, I., Varr\u00f3, D.: The Gamma statechart composition framework: design, verification and code generation for component-based reactive systems. In: ICSE, pp. 113\u2013116. ACM (2018). https:\/\/doi.org\/10.1145\/3183440.3183489","DOI":"10.1145\/3183440.3183489"},{"key":"5_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-78142-2_8","volume-title":"Coordination Models and Languages","author":"J Mota","year":"2021","unstructured":"Mota, J., Giunti, M., Ravara, A.: Java Typestate checker. In: Damiani, F., Dardha, O. (eds.) COORDINATION 2021. LNCS, vol. 12717, pp. 121\u2013133. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78142-2_8"},{"key":"5_CR62","doi-asserted-by":"publisher","unstructured":"Naeem, N.A., Lhot\u00e1k, O.: Typestate-like analysis of multiple interacting objects. In: Harris, G.E. (ed.) OOPSLA, pp. 347\u2013366. ACM (2008). https:\/\/doi.org\/10.1145\/1449764.1449792","DOI":"10.1145\/1449764.1449792"},{"key":"5_CR63","doi-asserted-by":"publisher","unstructured":"Nelaturu, K., Mavridou, A., Veneris, A.G., Laszka, A.: Verified development and deployment of multiple interacting smart contracts with VeriSolid. In: ICBC, pp. 1\u20139. IEEE (2020). https:\/\/doi.org\/10.1109\/ICBC48266.2020.9169428","DOI":"10.1109\/ICBC48266.2020.9169428"},{"key":"5_CR64","doi-asserted-by":"publisher","unstructured":"Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S.: A model checking framework for hierarchical systems. In: ASE, pp. 633\u2013636. IEEE (2011). https:\/\/doi.org\/10.1109\/ASE.2011.6100143","DOI":"10.1109\/ASE.2011.6100143"},{"key":"5_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48092-7_6","volume-title":"Correct System Design","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R.: Type and effect systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 114\u2013136. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48092-7_6"},{"key":"5_CR66","doi-asserted-by":"publisher","unstructured":"Par\u00edzek, P., Plasil, F., Kofron, J.: Model checking of software components: combining java pathfinder and behavior protocol model checker. In: Proceedings of SEW, pp. 133\u2013141. IEEE (2006). https:\/\/doi.org\/10.1109\/SEW.2006.23","DOI":"10.1109\/SEW.2006.23"},{"issue":"11","key":"5_CR67","doi-asserted-by":"publisher","first-page":"1056","DOI":"10.1109\/TSE.2002.1049404","volume":"28","author":"F Plasil","year":"2002","unstructured":"Plasil, F., Visnovsky, S.: Behavior protocols for software components. IEEE Trans. Software Eng. 28(11), 1056\u20131076 (2002). https:\/\/doi.org\/10.1109\/TSE.2002.1049404","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR68","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: In Transition From Global to Modular Temporal Reasoning about Programs. In: Apt, K.R. (ed.) LMCS. NATO ASI Series, vol. 13, pp. 123\u2013144. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"5_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-54415-1_49","volume-title":"Theoretical Aspects of Computer Software","author":"A Pnueli","year":"1991","unstructured":"Pnueli, A., Shalev, M.: What is in a step: on the semantics of statecharts. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 244\u2013264. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54415-1_49"},{"key":"5_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/11901433_18","volume-title":"Formal Methods and Software Engineering","author":"AW Roscoe","year":"2006","unstructured":"Roscoe, A.W., Wu, Z.: Verifying statemate statecharts using CSP and FDR. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 324\u2013341. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_18"},{"key":"5_CR71","doi-asserted-by":"publisher","unstructured":"Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: M\u00fcller, P. (ed.) ECOOP. LIPIcs, vol. 74, pp. 24:1\u201324:31. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.24","DOI":"10.4230\/LIPIcs.ECOOP.2017.24"},{"key":"5_CR72","doi-asserted-by":"publisher","unstructured":"Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: Krishnamurthi, S., Lerner, B.S. (eds.) ECOOP. LIPIcs, vol. 56, pp. 21:1\u201321:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2016.21","DOI":"10.4230\/LIPIcs.ECOOP.2016.21"},{"key":"5_CR73","doi-asserted-by":"crossref","unstructured":"Sipser, M.: Introduction to the Theory of Computation, 1st edn.. International Thomson Publishing (1996)","DOI":"10.1145\/230514.571645"},{"key":"5_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-24933-4_3","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"M Sirjani","year":"2011","unstructured":"Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20\u201356. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24933-4_3"},{"key":"5_CR75","doi-asserted-by":"publisher","unstructured":"Skalka, C.: Trace effects and object orientation. In: PPDP, pp. 139\u2013150. ACM (2005). https:\/\/doi.org\/10.1145\/1069774.1069787","DOI":"10.1145\/1069774.1069787"},{"issue":"2","key":"5_CR76","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1017\/S0956796807006466","volume":"18","author":"C Skalka","year":"2008","unstructured":"Skalka, C., Smith, S., Van Horn, D.: Types and trace effects of higher order programs. J. Funct. Program. 18(2), 179\u2013249 (2008). https:\/\/doi.org\/10.1017\/S0956796807006466","journal-title":"J. Funct. Program."},{"issue":"1","key":"5_CR77","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"RE Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157\u2013171 (1986). https:\/\/doi.org\/10.1109\/TSE.1986.6312929","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR78","doi-asserted-by":"publisher","unstructured":"Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, \u00c9.: First-class state change in plaid. In: Lopes, C.V., Fisher, K. (eds.) OOPSLA, pp. 713\u2013732. ACM (2011). https:\/\/doi.org\/10.1145\/2048066.2048122","DOI":"10.1145\/2048066.2048122"},{"key":"5_CR79","doi-asserted-by":"publisher","unstructured":"Tate, R.: The sequential semantics of producer effect systems. In: POPL, pp. 15\u201326. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429074","DOI":"10.1145\/2429069.2429074"},{"key":"5_CR80","first-page":"53","volume":"103","author":"VT Vasconcelos","year":"2011","unstructured":"Vasconcelos, V.T.: Sessions, from types to programming languages. Bull. EATCS 103, 53\u201373 (2011)","journal-title":"Bull. EATCS"},{"key":"5_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-030-50086-3_12","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"AL Voinea","year":"2020","unstructured":"Voinea, A.L., Dardha, O., Gay, S.J.: Typechecking Java protocols with [ST]Mungo. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 208\u2013224. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_12"},{"key":"5_CR82","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/eptcs.304.1","volume":"304","author":"H Zeng","year":"2019","unstructured":"Zeng, H., Kurz, A., Tuosto, E.: Interface automata for choreographies. Electron. Proc. Theor. Comput. Sci. 304, 1\u201319 (2019). https:\/\/doi.org\/10.4204\/eptcs.304.1","journal-title":"Electron. Proc. Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-35361-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T14:04:39Z","timestamp":1686751479000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-35361-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031353604","9783031353611"],"references-count":82,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-35361-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"15 June 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Languages and Models","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 June 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2023\/coordination","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}