{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:52:40Z","timestamp":1743105160143,"version":"3.40.3"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030760199"},{"type":"electronic","value":"9783030760205"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-76020-5_3","type":"book-chapter","created":{"date-parts":[[2021,6,3]],"date-time":"2021-06-03T23:06:17Z","timestamp":1622761577000},"page":"29-62","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Moded and Continuous Abstract State\u00a0Machines"],"prefix":"10.1007","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,4]]},"reference":[{"key":"3_CR1","unstructured":"Summit Report: Cyber-Physical Systems (2008). http:\/\/iccps2012.cse.wustl.edu\/_doc\/CPS_Summit_Report.pdf"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theoret. Comp. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comp. Sci."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Back, R.J., Petre, L., Porres, I.: Continuous action systems as a model for hybrid systems. Nordic J. Comp. 8, 2\u201321, 202\u2013213 (2001). Extended version of FTRTFT-00. LNCS 1926","DOI":"10.1007\/3-540-45352-0_17"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Banach, R., Zhu, H.: Language evolution and healthiness for critical cyber-physical systems. J. Soft. Evol. Proc. 2020, e2301, 24 (2021)","DOI":"10.1002\/smr.2301"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Barolli, L., Takizawa, M., Hussain, F.: Special issue on emerging trends in cyber-physical systems. J. Amb. Intel. Hum. Comput. 2, 249\u2013250 (2011)","DOI":"10.1007\/s12652-011-0062-2"},{"key":"3_CR9","unstructured":"Beauquier, D., Slissenko, A.: On Semantics of Algorithms with Continuous Time. Technical report TR-LACL-1997-15, LACL, University of Paris-12 (1997)"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Bender, K., Broy, M., P\u00e9ter, I., Pretschner, A., Stauner, T.: Model based development of hybrid systems: specification, simulation, test case generation. In: Engell, S., Frehse, G., Schnieder, E. (eds.) Modelling Analysis, and Design of Hybrid Systems, LNCIS, vol. 279, pp. 37\u201351. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45426-8_3","DOI":"10.1007\/3-540-45426-8_3"},{"key":"3_CR11","first-page":"237","volume":"15","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM refinement method. FACJ 15, 237\u2013257 (2003)","journal-title":"FACJ"},{"key":"3_CR12","unstructured":"B\u00f6rger, E., Gurevich, Y., Rosenzweig, D.: The bakery algorithm: yet another specification and verification. In: B\u00f6rger, E. (ed.) Specification and Validation Methods. Oxford University Press (1995)"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines. A Method for High Level System Design and Analysis. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-642-18216-7","DOI":"10.1007\/978-3-642-18216-7"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/1000000001","volume":"1","author":"L Carloni","year":"2006","unstructured":"Carloni, L., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.: Languages and tools for hybrid systems design. Found. Trends Electron. Design Autom. 1, 1\u2013193 (2006)","journal-title":"Found. Trends Electron. Design Autom."},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_1"},{"key":"3_CR16","unstructured":"Cohen, J., Slissenko, A.: Implementation of timed abstract state machines with instantaneous actions by machines with delays. Technical report, TR-LACL-2008-2, LACL, University of Paris-12 (2008)"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, London (2001). https:\/\/doi.org\/10.1007\/978-1-4471-0257-1","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"3_CR18","unstructured":"ESW: Embedded Systems Week Conferences"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Chen, M., Kr\u00f6ger, P.: In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-State Automata. ACM SIGLOG News 6, 19\u201339 (2019)","DOI":"10.1145\/3313909.3313913"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-49676-2_22","volume-title":"ZUM \u201998: The Z Formal Specification Notation","author":"V Friesen","year":"1998","unstructured":"Friesen, V., Nordwig, A., Weber, M.: Object-oriented specification of hybrid systems using UML$${^h}$$ and ZimOO. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 328\u2013346. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-540-49676-2_22"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Friesen, V., Nordwig, A., Weber, M.: Toward an object-oriented design methodology for hybrid systems. In: Object-Oriented Technology and Computing Systems Re-Engineering, pp. 1\u201315. Elsevier (1999)","DOI":"10.1533\/9781782420613.1"},{"key":"3_CR22","unstructured":"Geisberger, E., Broy, M. (eds.): Living in a Networked World. Integrated Research Agenda Cyber-Physical Systems (agendaCPS) (2015). http:\/\/www.acatech.de\/file admin\/user_upload\/Baumstruktur_nach_Website\/Acatech\/root\/de\/Publikationen\/Pro jektberichte\/acaetch_STUDIE_agendaCPS_eng_WEB.pdf"},{"key":"3_CR23","unstructured":"Graf, S., Prinz, A.: A framework for time in FDTs. In: Proceedings of FORTE-04. LNCS, vol. 1092, pp. 266\u2013290. Springer (2004)"},{"key":"3_CR24","first-page":"143","volume":"77","author":"S Graf","year":"2007","unstructured":"Graf, S., Prinz, A.: Time in abstract state machines. Fund. Inf. 77, 143\u2013174 (2007)","journal-title":"Fund. Inf."},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Gratzer, G.: Universal algebra. In: Abstract Algebra. Graduate Texts in Mathematics, vol. 242. Springer, New York (2007). https:\/\/doi.org\/10.1007\/978-0-387-71568-1_15","DOI":"10.1007\/978-0-387-71568-1_15"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-61377-3_43","volume-title":"Computer Science Logic","author":"Y Gurevich","year":"1996","unstructured":"Gurevich, Y., Huggins, J.K.: The railroad crossing problem: an experiment with instantaneous actions and immediate reactions. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 266\u2013290. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61377-3_43"},{"key":"3_CR27","unstructured":"He, J.: From CSP to hybrid systems. In: Roscoe (ed.) A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171\u2013189. Prentice-Hall (1994)"},{"key":"3_CR28","unstructured":"Henzinger, T.: The Theory of hybrid automata. In: Proceedings of IEEE LICS-96, pp. 278\u2013292. IEEE (1996). http:\/\/mtc.epfl.ch\/~tah\/Publications\/the_theory_of_hyb rid_automata.pdf"},{"key":"3_CR29","unstructured":"HSCC: Hybrid Systems: Command and Control Conferences"},{"key":"3_CR30","unstructured":"Karlsruhe Interactive Verifier. http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/ swt\/se\/kiv\/"},{"key":"3_CR31","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/BFb0020971","volume-title":"Hybrid Systems III","author":"N Lynch","year":"1996","unstructured":"Lynch, N., Segala, R., Vaandrager, F., Weinberg, H.B.: Hybrid I\/O automata. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 496\u2013510. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020971"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Lynch, N., Segala, R., Vaandrager, F.a.: Hybrid I\/O automata. Inf. Comput. 185, 105\u2013157. mIT Technical Report MIT-LCS-TR-827d","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"3_CR34","unstructured":"Maple. http:\/\/www.maplesoft.com"},{"key":"3_CR35","unstructured":"Mathematica. http:\/\/www.wolfram.com"},{"key":"3_CR36","unstructured":"National Science and Technology Council: Trustworthy Cyberspace: Strategic Plan for the Federal Cybersecurity Research and Development Program (2011). http:\/\/www.whitehouse.gov\/sites\/default\/files\/microsites\/ostp\/fed_cybersecurity_rd_ strategic_plan_2011.pdf"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14509-4","DOI":"10.1007\/978-3-642-14509-4"},{"key":"3_CR38","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Foundations of Hybrid Systems. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0","DOI":"10.1007\/978-3-319-63588-0"},{"key":"3_CR39","volume-title":"Handbook of Ordinary Differential Equations: Exact Solutions, Methods, and Problems","author":"A Polyanin","year":"2018","unstructured":"Polyanin, A., Zaitsev, V.: Handbook of Ordinary Differential Equations: Exact Solutions, Methods, and Problems. C.R.C. Press, Boca Raton (2018)"},{"key":"3_CR40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32027-9","volume-title":"Concurrent Programming: Algorithms, Principles and Foundations","author":"M Raynal","year":"2013","unstructured":"Raynal, M.: Concurrent Programming: Algorithms, Principles and Foundations. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-32027-9"},{"key":"3_CR41","unstructured":"Royden, H., Fitzpatrick, P.: Real Analysis. Pearson, London (2010)"},{"key":"3_CR42","unstructured":"Rust, H.: Hybrid abstract state machines: using the hyperreals for describing continuous changes in a discrete notation. Technical report. Proc. ASM-00, TIK Report 87, ETH Zurich (2000)"},{"key":"3_CR43","first-page":"952","volume":"7","author":"G Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. JUCS 7, 952\u2013979 (2001)","journal-title":"JUCS"},{"key":"3_CR44","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/j.tcs.2004.11.013","volume":"336","author":"G Schellhorn","year":"2005","unstructured":"Schellhorn, G.: ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theoret. Comp. Sci. 336, 403\u2013435 (2005)","journal-title":"Theoret. Comp. Sci."},{"key":"3_CR45","first-page":"1984","volume":"14","author":"A Slissenko","year":"2008","unstructured":"Slissenko, A., Vasilyev, P.: Simulation of timed abstract state machines with predicate logic model checking. JUCS 14, 1984\u20132006 (2008)","journal-title":"JUCS"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-16355-5_32","volume-title":"Ubiquitous Intelligence and Computing","author":"M-O Stehr","year":"2010","unstructured":"Stehr, M.-O., Kim, M., Talcott, C.: Toward distributed declarative control of networked cyber-physical systems. In: Yu, Z., Liscano, R., Chen, G., Zhang, D., Zhou, X. (eds.) UIC 2010. LNCS, vol. 6406, pp. 397\u2013413. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16355-5_32"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-21437-0_1","volume-title":"FM 2011: Formal Methods","author":"J Sztipanovits","year":"2011","unstructured":"Sztipanovits, J.: Model integration and cyber physical systems: a semantics perspective. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, p. 1. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_1"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Boston (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Walter, W.: Ordinary Differential Equations. Springer, New York (1998). https:\/\/doi.org\/10.1007\/978-1-4612-0601-9","DOI":"10.1007\/978-1-4612-0601-9"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Wechler, W.: Universal Algebra for Computer Scientists. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/978-3-642-76771-5","DOI":"10.1007\/978-3-642-76771-5"},{"key":"3_CR51","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s13174-010-0004-9","volume":"1","author":"J White","year":"2010","unstructured":"White, J., Clarke, S., Groba, C., Dougherty, B., Thompson, C., Schmidt, D.: R&D challenges and solutions for mobile cyber-physical applications and supporting internet services. J. Internet Serv. Appl. 1, 45\u201356 (2010)","journal-title":"J. Internet Serv. Appl."},{"key":"3_CR52","unstructured":"Wikipedia: Absolute continuity"},{"key":"3_CR53","unstructured":"Willems, J.: Open Dynamical Systems: Their Aims and their Origins. Ruberti Lecture, Rome (2007). http:\/\/homes.esat.kuleuven.be\/~jwillems\/Lectures\/2007\/Ruberti lecture.pdf"},{"key":"3_CR54","volume-title":"Using Z, Specification, Refinement and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z, Specification, Refinement and Proof. Prentice Hall, Hoboken (1996)"},{"key":"3_CR55","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-24106-2_50","volume-title":"Convergence and Hybrid Information Technology","author":"L Zhang","year":"2011","unstructured":"Zhang, L., He, J.: A formal framework for aspect-oriented specification of cyber physical systems. In: Lee, G., Howard, D., \u015al\u0119zak, D. (eds.) ICHIT 2011. CCIS, vol. 206, pp. 391\u2013398. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24106-2_50"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Zhlke, L., Ollinger, L.: Agile automaton systems based on cyber-physical systems and service oriented architectures. In: Lee, G. (ed.) Proceedings of ICAR-11, LNEE, vol. 122, pp. 567\u2013574. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25553-3_70","DOI":"10.1007\/978-3-642-25553-3_70"}],"container-title":["Lecture Notes in Computer Science","Logic, Computation and Rigorous Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-76020-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T14:20:03Z","timestamp":1709821203000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-76020-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030760199","9783030760205"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-76020-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"4 June 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}