{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T22:44:00Z","timestamp":1763765040426,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031851339"},{"type":"electronic","value":"9783031851346"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-85134-6_8","type":"book-chapter","created":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T04:01:57Z","timestamp":1742443317000},"page":"182-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Animating Rebeca"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice\u00a0H.","family":"ter Beek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0971-8919","authenticated-orcid":false,"given":"Jos\u00e9","family":"Proen\u00e7a","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,3,21]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Aceto, L., Cimini, M., Ing\u00f3lfsd\u00f3ttir, A., Reynisson, A.H., Sigurdarson, S.H., Sirjani, M.: Modelling and simulation of asynchronous real-time systems using timed Rebeca. In: Mousavi, M.R., Ravara, A. (eds.) Proceedings of the 10th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA\u201911). EPTCS, vol.\u00a058, pp. 1\u201319 (2011). https:\/\/doi.org\/10.4204\/EPTCS.58.1","DOI":"10.4204\/EPTCS.58.1"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Agha, G.A.: ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence, MIT Press (1986). https:\/\/doi.org\/10.7551\/mitpress\/1086.001.0001","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/BFb0084816","volume-title":"CONCUR \u201992","author":"G Agha","year":"1992","unstructured":"Agha, G., Mason, I.A., Smith, S., Talcott, C.: Towards a theory of actor computation. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 565\u2013579. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0084816"},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S095679689700261X","volume":"7","author":"GA Agha","year":"1997","unstructured":"Agha, G.A., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7(1), 1\u201372 (1997). https:\/\/doi.org\/10.1017\/S095679689700261X","journal-title":"J. Funct. Program."},{"issue":"4","key":"8_CR5","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/3702231","volume":"15","author":"M ter Beek","year":"2024","unstructured":"ter Beek, M., Broy, M., Dongol, B.: The role of formal methods in computer science education. ACM Inroads 15(4), 58\u201366 (2024). https:\/\/doi.org\/10.1145\/3702231","journal-title":"ACM Inroads"},{"key":"8_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-031-27481-7_9","volume-title":"FM 2023","author":"MH ter Beek","year":"2023","unstructured":"ter Beek, M.H., Cledou, G., Hennicker, R., Proen\u00e7a, J.: Can we communicate? Using dynamic logic to verify team automata. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 122\u2013141. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_9"},{"key":"8_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-031-62697-5_10","volume-title":"COORDINATION 2024","author":"MH ter Beek","year":"2024","unstructured":"ter Beek, M.H., Hennicker, R., Proen\u00e7a, J.: Team automata: overview and roadmap. In: Castellani, I., Tiezzi, F. (eds.) COORDINATION 2024. LNCS, vol. 14676, pp. 161\u2013198. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-62697-5_10"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Cledou, G., Edixhoven, L., Jongmans, S.S., Proen\u00e7a, J.: API generation for multiparty session types, revisited and revised using Scala\u00a03. In: Ali, K., Vitek, J. (eds.) Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP\u201922). LIPIcs, vol.\u00a0222, pp. 27:1\u201327:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.27","DOI":"10.4230\/LIPIcs.ECOOP.2022.27"},{"key":"8_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-031-20872-0_11","volume-title":"FACS 2022","author":"L Edixhoven","year":"2022","unstructured":"Edixhoven, L., Jongmans, S.S.: Realisability of branching pomsets. In: Tapia Tarifa, S.L., Proen\u00e7a, J. (eds.) FACS 2022. LNCS, vol. 13712, pp. 185\u2013204. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-20872-0_11"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Edixhoven, L., Jongmans, S.S., Proen\u00e7a, J., Cledou, G.: Branching pomsets for choreographies. In: Aubert, C., Di\u00a0Giusto, C., Safina, L., Scalas, A. (eds.) Proceedings of the 15th Interaction and Concurrency Experience (ICE 2022). EPTCS, vol.\u00a0365, pp. 37\u201352 (2022). https:\/\/doi.org\/10.4204\/EPTCS.365.3","DOI":"10.4204\/EPTCS.365.3"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Fredlund, L., Svensson, H.: McErlang: a model checker for a distributed functional programming language. In: Proceedings of the 12th International Conference on Functional Programming (ICFP 2007), pp. 125\u2013136. ACM (2007). https:\/\/doi.org\/10.1145\/1291151.1291171","DOI":"10.1145\/1291151.1291171"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2020","unstructured":"Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 3\u201369. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1"},{"key":"8_CR13","unstructured":"Hewitt, C.: Description and Theoretical Analysis (Using Schemata) of Planner: A Language for Proving Theorems and Manipulating Models in a Robot. Technical report AITR-258, MIT (1972), http:\/\/hdl.handle.net\/1721.1\/6916"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Hojjat, H., Sirjani, M., Mousavi, M.R., Groote, J.F.: Sarir: a Rebeca to mCRL2 translator. In: Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD 2007), pp. 216\u2013222. IEEE (2007). https:\/\/doi.org\/10.1109\/ACSD.2007.62","DOI":"10.1109\/ACSD.2007.62"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/J.SCICO.2016.03.004","volume":"128","author":"A Jafari","year":"2016","unstructured":"Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: PTRebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22\u201350 (2016). https:\/\/doi.org\/10.1016\/J.SCICO.2016.03.004","journal-title":"Sci. Comput. Program."},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: the model-checking engine of Rebeca. In: Proceedings of the 21st Symposium on Applied Computing (SAC 2006), pp. 1810\u20131815. ACM (2006). https:\/\/doi.org\/10.1145\/1141277.1141704","DOI":"10.1145\/1141277.1141704"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-23703-5_1","volume-title":"Cyber Physical Systems. Model-Based Design","author":"I Jahandideh","year":"2019","unstructured":"Jahandideh, I., Ghassemi, F., Sirjani, M.: Hybrid Rebeca: modeling and analyzing of cyber-physical systems. In: Chamberlain, R., Taha, W., T\u00f6rngren, M. (eds.) CyPhy\/WESE -2018. LNCS, vol. 11615, pp. 3\u201327. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23703-5_1"},{"key":"8_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-031-19849-6_26","volume-title":"ISoLA 2022","author":"SS Jongmans","year":"2022","unstructured":"Jongmans, S.S., Proen\u00e7a, J.: ST4MP: a blueprint of multiparty session typing for multilingual programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13701, pp. 460\u2013478. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_26"},{"key":"8_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-031-42441-0_6","volume-title":"FSEN 2023","author":"E Khamespanah","year":"2023","unstructured":"Khamespanah, E., Sirjani, M., Khosravi, R.: Afra: an Eclipse-based tool with extensible architecture for modeling and model checking of Rebeca family models. In: Hojjat, H., \u00c1brah\u00e1m, E. (eds.) FSEN 2023. LNCS, vol. 14155, pp. 72\u201387. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-42441-0_6"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/J.SCICO.2014.07.005","volume":"98","author":"E Khamespanah","year":"2015","unstructured":"Khamespanah, E., Sirjani, M., Sabahi-Kaviani, Z., Khosravi, R., Izadi, M.: Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci. Comput. Program. 98, 184\u2013204 (2015). https:\/\/doi.org\/10.1016\/J.SCICO.2014.07.005","journal-title":"Sci. Comput. Program."},{"key":"8_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-031-51060-1_9","volume-title":"Active Object Languages: Current Research Trends","author":"R Khosravi","year":"2024","unstructured":"Khosravi, R., Khamespanah, E., Ghassemi, F., Sirjani, M.: Actors upgraded for variability, adaptability, and determinism. In: de Boer, F.S., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Kamburjan, E. (eds.) Active Object Languages: Current Research Trends. LNCS, vol. 14360, pp. 226\u2013260. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-51060-1_9"},{"key":"8_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-031-35361-1_9","volume-title":"COORDINATION 2023","author":"J Proen\u00e7a","year":"2023","unstructured":"Proen\u00e7a, J., Edixhoven, L.: Caos: a reusable scala web animator of operational semantics. In: Jongmans, S.S., Lopes, A. (eds.) COORDINATION 2023. LNCS, vol. 13908, pp. 163\u2013171. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35361-1_9"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/J.SCICO.2014.01.008","volume":"89","author":"AH Reynisson","year":"2014","unstructured":"Reynisson, A.H., et al.: Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Sci. Comput. Program. 89, 41\u201368 (2014). https:\/\/doi.org\/10.1016\/J.SCICO.2014.01.008","journal-title":"Sci. Comput. Program."},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74792-5_5","volume-title":"Formal Methods for Components and Objects","author":"M Sirjani","year":"2007","unstructured":"Sirjani, M.: Rebeca: theory, applications, and tools. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 102\u2013126. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74792-5_5"},{"key":"8_CR25","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":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-319-30734-3_25","volume-title":"Theory and Practice of Formal Methods","author":"M Sirjani","year":"2016","unstructured":"Sirjani, M., Khamespanah, E.: On time actors. In: \u00c1brah\u00e1m, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 373\u2013392. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30734-3_25"},{"key":"8_CR27","unstructured":"Sirjani, M., Movaghar, A.: An Actor-Based Model for Reactive Systems: Rebeca. Technical report CS-TR-80-01, Sharif University of Technology (2001)"},{"key":"8_CR28","unstructured":"Sirjani, M., Movaghar, A., Mousavi, M.R.: Compositional verification of an actor-based model for reactive systems. In: Proceedings of the 1st Workshop on Automated Verification of Critical Systems (AVoCS 2001), pp. 114\u2013118. Oxford University (2001). https:\/\/rebeca-lang.org\/assets\/papers\/2001\/CompositionalVerificationOfAnObject-BasedModelForReactiveSystems.pdf"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Sirjani, M., Shali, A., Jaghoori, M.M., Iravanchi, H., Movaghar, A.: A front-end tool for automated abstraction and modular verification of actor-based models. In: Proceedings of the 4th International Conference on Application of Concurrency to System Design (ACSD 2004), pp. 145\u2013150. IEEE (2004). https:\/\/doi.org\/10.1109\/CSD.2004.1309125","DOI":"10.1109\/CSD.2004.1309125"},{"key":"8_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-031-71261-6_6","volume-title":"FACS 2024","author":"D Tinoco","year":"2024","unstructured":"Tinoco, D., Madeira, A., Martins, M.A., Proen\u00e7a, J.: Reactive graphs in action. In: Marmsoler, D., Sun, M. (eds.) FACS 2024. LNCS, vol. 15189, pp. 97\u2013105. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71261-6_6"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-34281-3_12","volume-title":"Formal Methods and Software Engineering","author":"M Varshosaz","year":"2012","unstructured":"Varshosaz, M., Khosravi, R.: Modeling and verification of probabilistic actor systems using pRebeca. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 135\u2013150. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34281-3_12"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Zakeriyan, A., Khamespanah, E., Sirjani, M., Khosravi, R.: Jacco: more efficient model checking toolset for Java actor programs. In: Boix, E.G., Haller, P., Ricci, A., Varela, C.A. (eds.) Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE! 2015), pp. 37\u201344. ACM (2015). https:\/\/doi.org\/10.1145\/2824815.2824819","DOI":"10.1145\/2824815.2824819"}],"container-title":["Lecture Notes in Computer Science","Rebeca for Actor Analysis in Action"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-85134-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T08:35:23Z","timestamp":1743496523000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-85134-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031851339","9783031851346"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-85134-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 March 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}