{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:02:10Z","timestamp":1786978930394,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":25,"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_9","type":"book-chapter","created":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T00:01:22Z","timestamp":1742428882000},"page":"195-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verify Engineering Models, Not Scientific Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6885-5572","authenticated-orcid":false,"given":"Shaokai","family":"Lin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5663-0584","authenticated-orcid":false,"given":"Edward A.","family":"Lee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,3,21]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G.: ACTORS: A Model of Concurrent Computation in Distributed Systems. The MIT Press Series in Artificial Intelligence, MIT Press, Cambridge, MA (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"issue":"9","key":"9_CR2","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1145\/83880.84528","volume":"33","author":"G Agha","year":"1990","unstructured":"Agha, G.: Concurrent object-oriented programming. Commun. ACM 33(9), 125\u2013140 (1990)","journal-title":"Commun. ACM"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Agha, G.A.: Abstracting interaction patterns: a programming paradigm for open distributed systems. In: Stefani, E.N., J.-B. (eds.) Formal Methods for Open Object-based Distributed Systems, IFIP Transactions, pp. 135\u2013153. Chapman and Hall (1997). https:\/\/doi.org\/10.1007\/978-0-387-35082-0_10","DOI":"10.1007\/978-0-387-35082-0_10"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Bateni, S., et alisk and mitigation of nondeterminism in distributed cyber-physical systems. In: ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE) (2023). https:\/\/doi.org\/10.1145\/3610579.3613219","DOI":"10.1145\/3610579.3613219"},{"issue":"1","key":"9_CR5","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., De Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64\u201383 (2003)","journal-title":"Proc. IEEE"},{"key":"9_CR6","volume-title":"Empirical Model-Building and Response Surfaces","author":"GEP Box","year":"1987","unstructured":"Box, G.E.P., Draper, N.R.: Empirical Model-Building and Response Surfaces. Wiley Series in Probability and Statistics, Wiley, Hoboken (1987)"},{"key":"9_CR7","unstructured":"Cataldo, A., Lee, E.A., Liu, X., Matsikoudis, E., Zheng, H.: A constructive fixed-point theorem and the feedback semantics of timed systems. In: Workshop on Discrete Event Systems (WODES) (2006). http:\/\/ptolemy.eecs.berkeley.edu\/publications\/papers\/06\/constructive\/"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0004-3702(77)90033-9","volume":"8","author":"C Hewitt","year":"1977","unstructured":"Hewitt, C.: Viewing control structures as patterns of passing messages. J. Artif. Intell. 8(3), 323\u2013363 (1977)","journal-title":"J. Artif. Intell."},{"key":"9_CR9","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., Damiani, F., H\u00e4hnle, R., Broch Johnsen, E., 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":"9_CR10","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-24349-3_5","volume-title":"Advances in Real-Time Systems","author":"CM Kirsch","year":"2012","unstructured":"Kirsch, C.M., Sokolova, A.: The logical execution time paradigm. In: Chakraborty, S., Ebersp\u00e4cher, J. (eds.) Advances in Real-Time Systems, pp. 103\u2013120. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-24349-3_5"},{"issue":"5","key":"9_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3453652","volume":"20","author":"EA Lee","year":"2021","unstructured":"Lee, E.A.: Determinism. ACM Trans. Embed. Comput. Syst. (TECS) 20(5), 1\u201334 (2021). https:\/\/doi.org\/10.1145\/3453652","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Lee, E.A., Akella, R., Bateni, S., Lin, S., Lohstroh, M., Menard, C.: Consistency vs. availability in distributed cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 22(5s), 1\u201324 (2023). https:\/\/doi.org\/10.1145\/3609119. presented at EMSOFT, September 17-22, 2023, Hamburg, Germany","DOI":"10.1145\/3609119"},{"key":"9_CR13","unstructured":"Lee, E.A., Liu, J., Muliadi, L., Zheng, H.: Discrete-event models. In: Ptolemaeus, C. (ed.) System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, Berkeley, CA (2014). http:\/\/ptolemy.org\/books\/Systems"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Lee, E.A., Sirjani, M.: What good are models? In: Formal Aspects of Component Software (FACS). vol. LNCS 11222. Springer (2018)","DOI":"10.1007\/978-3-030-02146-7_1"},{"key":"9_CR15","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/11180.001.0001","volume-title":"Plato and the Nerd \u2013 The Creative Partnership of Humans and Technology","author":"EA Lee","year":"2017","unstructured":"Lee, E.A.: Plato and the Nerd \u2013 The Creative Partnership of Humans and Technology. MIT Press, Cambridge (2017)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Liao, S., Tjiang, S., Gupta, R.: An efficient implementation of reactivity for modeling hardware in the scenic design environment. In: Proceedings of the 34th annual Design Automation Conference, pp. 70\u201375 (1997)","DOI":"10.1145\/266021.266037"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-030-41131-2_4","volume-title":"Cyber Physical Systems. Model-Based Design","author":"M Lohstroh","year":"2020","unstructured":"Lohstroh, M., Romeo, \u00cd.\u00cd., Goens, A., Derler, P., Castrillon, J., Lee, E.A., Sangiovanni-Vincentelli, A.: Reactors: a deterministic model for composable reactive systems. In: Chamberlain, R., Edin Grimheden, M., Taha, W. (eds.) CyPhy\/WESE -2019. LNCS, vol. 11971, pp. 59\u201385. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41131-2_4"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Lohstroh, M., Lee, E.A., Edwards, S., Broman, D.: Logical time for reactive software. In: Workshop on Timing-Centric Reactive Software (TCRS), in Cyber-Physical Systems and Internet of Things Week (CPSIoT). ACM (2023). https:\/\/doi.org\/10.1145\/3576914.3587494","DOI":"10.1145\/3576914.3587494"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a lingua franca for deterministic concurrent systems. ACM Trans. Embed. Comput. Syst. (TECS) 20(4), Article 36 (2021). https:\/\/doi.org\/10.1145\/3448128","DOI":"10.1145\/3448128"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/BFb0032003","volume-title":"Real-Time: Theory in Practice","author":"O Maler","year":"1992","unstructured":"Maler, O., Manna, Z., Pnueli, A.: Prom timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 447\u2013484. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0032003"},{"key":"9_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":"9_CR22","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":"9_CR23","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":"9_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3390\/math8071068","volume":"8","author":"M Sirjani","year":"2020","unstructured":"Sirjani, M., Lee, E.A., Khamespanah, E.: Verification of cyberphysical systems. Mathematics 8, 1\u201320 (2020). https:\/\/doi.org\/10.3390\/math8071068","journal-title":"Mathematics"},{"issue":"3","key":"9_CR25","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/99.615432","volume":"4","author":"BP Zeigler","year":"1997","unstructured":"Zeigler, B.P., Moon, Y., Kim, D., Ball, G.: The DEVS environment for high-performance modeling and simulation. IEEE Comput. Sci. Eng. 4(3), 61\u201371 (1997)","journal-title":"IEEE Comput. Sci. Eng."}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T04:37:13Z","timestamp":1743482233000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-85134-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031851339","9783031851346"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-85134-6_9","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"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}