{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T12:19:04Z","timestamp":1784204344767,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031851339","type":"print"},{"value":"9783031851346","type":"electronic"}],"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_2","type":"book-chapter","created":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T04:01:44Z","timestamp":1742443304000},"page":"26-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["20 Years of\u00a0Actor Model Checking with\u00a0Rebeca From Dining Philosophers to\u00a0Micro-services"],"prefix":"10.1007","author":[{"given":"Ehsan","family":"Khamespanah","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammad Mahdi","family":"Jaghoori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,3,21]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","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":"2_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MS.2016.64","volume":"33","author":"A Balalaie","year":"2016","unstructured":"Balalaie, A., Heydarnoori, A., Jamshidi, P.: Microservices architecture enables devops: migration to a cloud-native architecture. IEEE Softw. 33(3), 42\u201352 (2016)","journal-title":"IEEE Softw."},{"key":"2_CR4","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-030-59155-7_31","volume-title":"Software Architecture","author":"M Camilli","year":"2020","unstructured":"Camilli, M.: Continuous formal verification of microservice-based process flows. In: Muccini, H., et al. (eds.) ECSA 2020. CCIS, vol. 1269, pp. 420\u2013435. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59155-7_31"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jha, S., Peled, D.: Combining partial order and symmetry reductions. In: Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS 1997. LNCS, vol.\u00a01217, pp. 19\u201334. Springer, Cham (1997)","DOI":"10.1007\/BFb0035378"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Ph.D. thesis, Universite De Liege (1995)","DOI":"10.1007\/3-540-60761-7"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D Guck","year":"2012","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8\u201323. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_4"},{"key":"2_CR8","unstructured":"Hightower, K., Burns, B., Beda, J.: Kubernetes: Up and Running Dive into the Future of Infrastructure. O\u2019Reilly Media, Inc., Sebastopol (2017)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Nakhost, H., Sirjani, M.: Formal verification of the IEEE 802.1d spanning tree protocol using extended Rebeca. In: Arbab, F., Sirjani, M. (eds.) Proceedings of the First IPM International Workshop on Foundations of Software Engineering, FSEN 2005, Tehran, Iran, 1\u20133 October 2005. Electronic Notes in Theoretical Computer Science, vol.\u00a0159, pp. 139\u2013154. Elsevier (2005)","DOI":"10.1016\/j.entcs.2005.12.066"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Sirjani, M., Mousavi, M.R., Groote, J.F.: Sarir: a Rebeca to mCRL2 translator. In: Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), Bratislava, Slovak Republic, 10\u201313 July 2007, pp. 216\u2013222. IEEE Computer Society (2007)","DOI":"10.1109\/ACSD.2007.24"},{"key":"2_CR11","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)","journal-title":"Sci. Comput. Program."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: the model-checking engine of Rebeca. In: Haddad, H. (ed.) Proceedings of the ACM Symposium on Applied Computing (SAC 2006), Dijon, France, 23\u201327 April, pp. 1810\u20131815. ACM (2006)","DOI":"10.1145\/1141277.1141704"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s00236-009-0111-x","volume":"47","author":"MM Jaghoori","year":"2010","unstructured":"Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Khamespanah, E., Movaghar, A.: Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica 47(1), 33\u201366 (2010)","journal-title":"Acta Informatica"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/11604655_56","volume-title":"Distributed Computing and Internet Technology","author":"MM Jaghoori","year":"2005","unstructured":"Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Movaghar, A.: Efficient symmetry reduction for an actor-based model. In: Chakraborty, G. (ed.) ICDCIT 2005. LNCS, vol. 3816, pp. 494\u2013507. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11604655_56"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Jahandideh, I., Ghassemi, F., Sirjani, M.: Hybrid Rebeca: modeling and analyzing of cyber-physical systems. In: Cyber Physical Systems. Model-Based Design: 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Turin, Italy, 4\u20135 October 2018, Revised Selected Papers 8, pp. 3\u201327. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-23703-5_1"},{"issue":"11","key":"2_CR16","doi-asserted-by":"publisher","first-page":"2476","DOI":"10.1002\/spe.3135","volume":"52","author":"SNA Jawaddi","year":"2022","unstructured":"Jawaddi, S.N.A., Johari, M.H., Ismail, A.: A review of microservices autoscaling with formal verification perspective. Softw. Pract. Exp. 52(11), 2476\u20132495 (2022)","journal-title":"Softw. Pract. Exp."},{"key":"2_CR17","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., Kaviani, Z.S., Khosravi, R., Izadi, M.J.: Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci. Comput. Program. 98, 184\u2013204 (2015)","journal-title":"Sci. Comput. Program."},{"key":"2_CR18","doi-asserted-by":"crossref","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: Fundamentals of Software Engineering - 10th International Conference, FSEN 2023, Tehran, Iran, 4\u20135 May 2023, Revised Selected Papers. Lecture Notes in Computer Science, vol. 14155, pp. 72\u201387. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-42441-0_6"},{"key":"2_CR19","unstructured":"Kreps, J., Narkhede, N., Rao, J., et\u00a0al.: Kafka: a distributed messaging system for log processing. In: Proceedings of the NetDB, Athens, Greece, vol.\u00a011, pp.\u00a01\u20137 (2011)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-75698-9_8","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"N Razavi","year":"2007","unstructured":"Razavi, N., Sirjani, M.: Compositional semantics of system-level designs written in SystemC. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 113\u2013128. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75698-9_8"},{"key":"2_CR21","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":"2_CR22","doi-asserted-by":"publisher","unstructured":"Sabahi-Kaviani, Z., Khosravi, R., \u00d6lveczky, P.C., Khamespanah, E., Sirjani, M.: Formal semantics and efficient analysis of timed Rebeca in real-time maude. Sci. Comput. Program. 113, 85\u2013118 (2015). https:\/\/doi.org\/10.1016\/J.SCICO.2015.07.003","DOI":"10.1016\/J.SCICO.2015.07.003"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Sinha, S., Kang, E.: Formal modeling and analysis of apache kafka in alloy 6. In: International Conference on Rigorous State-Based Methods, pp. 25\u201342. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-63790-2_2"},{"issue":"4","key":"2_CR24","first-page":"1052","volume":"3","author":"M Sirjani","year":"2004","unstructured":"Sirjani, M., SeyedRazi, H., Movaghar, A., Jaghoori, M.M., Forghanizadeh, S., Mojdeh, M.: Model checking CSMA\/CD protocol using an actor-based language. WSEAS Trans. Circuit Syst. 3(4), 1052\u20131057 (2004)","journal-title":"WSEAS Trans. Circuit Syst."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Formal Modeling: Actors, Open Systems, Biological Systems: Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, pp. 20\u201356 (2011)","DOI":"10.1007\/978-3-642-24933-4_3"},{"key":"2_CR26","unstructured":"Sirjani, M., Movaghar, A., Iravanchi, H., Jaghoori, M.M., Shali, A.: Model checking in Rebeca. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2003, Las Vegas, Nevada, USA, 23\u201326 June, vol. 4, pp. 1819\u20131822. CSREA Press (2003)"},{"issue":"6","key":"2_CR27","first-page":"1054","volume":"11","author":"M Sirjani","year":"2005","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Model checking, automated abstraction and compositional verification of Rebeca models. J. Univ. Comput. Sci. (JUCS) 11(6), 1054\u20131082 (2005)","journal-title":"J. Univ. Comput. Sci. (JUCS)"},{"issue":"4","key":"2_CR28","first-page":"385","volume":"63","author":"M Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., De Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fund. Inform. 63(4), 385\u2013410 (2004)","journal-title":"Fund. Inform."},{"key":"2_CR29","doi-asserted-by":"crossref","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 International Conference on Application of Concurrency to System Design (ACSD 2004), Hamilton, Canada, 16\u201318 June, pp. 145\u2013150. IEEE Computer Society (2004)","DOI":"10.1109\/CSD.2004.1309125"},{"key":"2_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.csi.2017.11.007","volume":"58","author":"A Souri","year":"2018","unstructured":"Souri, A., Navimipour, N.J., Rahmani, A.M.: Formal verification approaches and standards in the cloud computing: a comprehensive and systematic review. Comput. Stand. Interfaces 58, 1\u201322 (2018)","journal-title":"Comput. Stand. Interfaces"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Sun, M., Chen, Z.: Formal modeling and verification of kafka producer-consumer communication in mediator. In: Science and Information Conference, pp. 603\u2013619. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-62281-6_41"},{"key":"2_CR32","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2023.111750","volume":"203","author":"G Turin","year":"2023","unstructured":"Turin, G., Borgarelli, A., Donetti, S., Damiani, F., Johnsen, E.B., Tarifa, S.L.T.: Predicting resource consumption of kubernetes container systems using resource models. J. Syst. Softw. 203, 111750 (2023)","journal-title":"J. Syst. Softw."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Varshosaz, M., Khosravi, R.: Modeling and verification of probabilistic actor systems using prebeca. In: ICFEM, pp. 135\u2013150. Springer, Cham (2012)","DOI":"10.1007\/978-3-642-34281-3_12"},{"issue":"1","key":"2_CR34","doi-asserted-by":"publisher","first-page":"277","DOI":"10.2298\/CSIS210707057X","volume":"20","author":"J Xu","year":"2023","unstructured":"Xu, J., Yin, J., Zhu, H., Xiao, L.: Formalization and verification of Kafka messaging mechanism using CSP. Comput. Sci. Inf. Syst. 20(1), 277\u2013306 (2023)","journal-title":"Comput. Sci. Inf. Syst."}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T08:36:57Z","timestamp":1743496617000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-85134-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031851339","9783031851346"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-85134-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 March 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}