{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:54:14Z","timestamp":1742979254528,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031150760"},{"type":"electronic","value":"9783031150777"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-15077-7_2","type":"book-chapter","created":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T05:02:57Z","timestamp":1661144577000},"page":"24-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Monitoring Cyber-Physical Systems Using a\u00a0Tiny Twin to\u00a0Prevent Cyber-Attacks"],"prefix":"10.1007","author":[{"given":"Fereidoun","family":"Moradi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maryam","family":"Bagheri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanieh","family":"Rahmati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hamed","family":"Yazdi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sara Abbaspour","family":"Asadollah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,23]]},"reference":[{"key":"2_CR1","unstructured":"Afra: An integrated environment for modeling and verifying Rebeca family designs (2021). https:\/\/rebeca-lang.org\/alltools\/Afra. Accessed 09 July 2021"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Abera, T., et al.: C-FLAT: control-flow attestation for embedded systems software. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 743\u2013754 (2016)","DOI":"10.1145\/2976749.2978358"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.jss.2018.05.034","volume":"143","author":"M Bagheri","year":"2018","unstructured":"Bagheri, M., et al.: Coordinated actor model of self-adaptive track-based traffic control systems. J. Syst. Softw. 143, 116\u2013139 (2018)","journal-title":"J. Syst. Softw."},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-32759-9_9","volume-title":"FM 2012: Formal Methods","author":"H Barringer","year":"2012","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68\u201384. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_9"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.automatica.2018.07.017","volume":"97","author":"LK Carvalho","year":"2018","unstructured":"Carvalho, L.K., Wu, Y.C., Kwong, R., Lafortune, S.: Detection and mitigation of classes of attacks in supervisory control systems. Automatica 97, 121\u2013133 (2018)","journal-title":"Automatica"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Cheng, B.H.C., et al.: Using models at runtime to address assurance for self-adaptive systems. In: Bencomo, N., France, R., Cheng, B.H.C., A\u00dfmann, U. (eds.) Models@run.time. LNCS, vol. 8378, pp. 101\u2013136. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08915-7_4","DOI":"10.1007\/978-3-319-08915-7_4"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"825","DOI":"10.1109\/TDSC.2019.2906161","volume":"18","author":"L Cheng","year":"2019","unstructured":"Cheng, L., Tian, K., Yao, D., Sha, L., Beyah, R.A.: Checking is believing: event-aware program anomaly detection in cyber-physical systems. IEEE Trans. Dependable Secure Comput. 18(2), 825\u2013842 (2019)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2491245","volume":"31","author":"JC Corbett","year":"2013","unstructured":"Corbett, J.C., et al.: Spanner: Google\u2019s globally distributed database. ACM Trans. Comput. Syst. 31(3), 1\u201322 (2013)","journal-title":"ACM Trans. Comput. Syst."},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-45477-1_1","volume-title":"Computer Safety, Reliability, and Security","author":"L Dureuil","year":"2016","unstructured":"Dureuil, L., Petiot, G., Potet, M.-L., Le, T.-H., Crohen, A., de Choudens, P.: FISSC: a fault injection and simulation secure\u00a0collection. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 3\u201311. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45477-1_1"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Eckhart, M., Ekelhart, A.: A specification-based state replication approach for digital twins. In: Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and Privacy, pp. 36\u201347 (2018)","DOI":"10.1145\/3264888.3264892"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Gao, C., Seatzu, C., Li, Z., Giua, A.: Multiple attacks detection on discrete event systems. In: 2019 IEEE International Conference on Systems, Man and Cybernetics (SMC), pp. 2352\u20132357. IEEE (2019)","DOI":"10.1109\/SMC.2019.8914035"},{"issue":"3","key":"2_CR12","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. Artif. Intell. 8(3), 323\u2013364 (1977)","journal-title":"Artif. Intell."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-45237-7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DN Jansen","year":"2020","unstructured":"Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: An O(m\u00a0log\u00a0n) algorithm for branching bisimilarity on labelled transition systems. In: TACAS 2020. LNCS, vol. 12079, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_1"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Kang, E., Adepu, S., Jackson, D., Mathur, A.P.: Model-based security analysis of a water treatment system. In: Proceedings of Software Engineering for Smart Cyber-Physical Systems, pp. 22\u201328. ACM (2016)","DOI":"10.1145\/2897035.2897041"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Kassem, A., Falcone, Y.: Detecting fault injection attacks with runtime verification. In: Proceedings of the 3rd ACM Workshop on Software Protection, pp. 65\u201376 (2019)","DOI":"10.1145\/3338503.3357724"},{"key":"2_CR16","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)","journal-title":"Sci. Comput. Program."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"K\u0159ikava, F., Collet, P., France, R.B.: Actor-based runtime model of adaptable feedback control loops. In: Proceedings of the 7th Workshop on Models@ run. time, pp. 39\u201344 (2012)","DOI":"10.1145\/2422518.2422525"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.tcs.2021.08.021","volume":"890","author":"R Lanotte","year":"2021","unstructured":"Lanotte, R., Merro, M., Munteanu, A.: A process calculus approach to detection and mitigation of PLC malware. Theoret. Comput. Sci. 890, 125\u2013146 (2021)","journal-title":"Theoret. Comput. Sci."},{"issue":"9","key":"2_CR19","doi-asserted-by":"publisher","first-page":"8886","DOI":"10.1109\/JIOT.2020.2996663","volume":"7","author":"E Lee","year":"2020","unstructured":"Lee, E., Seo, Y.D., Kim, Y.G.: A cache-based model abstraction and runtime verification for the internet-of-things applications. IEEE Internet Things J. 7(9), 8886\u20138901 (2020)","journal-title":"IEEE Internet Things J."},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1), 2\u201316 (2005)","journal-title":"Int. J. Inf. Secur."},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"12333","DOI":"10.1016\/j.ifacol.2017.08.2161","volume":"50","author":"PM Lima","year":"2017","unstructured":"Lima, P.M., Alves, M.V., Carvalho, L.K., Moreira, M.V.: Security against network attacks in supervisory control systems. IFAC-PapersOnLine 50(1), 12333\u201312338 (2017)","journal-title":"IFAC-PapersOnLine"},{"issue":"4","key":"2_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3448128","volume":"20","author":"M Lohstroh","year":"2021","unstructured":"Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a Lingua Franca for deterministic concurrent systems. ACM Trans. Embed. Comput. Syst. 20(4), 1\u201327 (2021)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Lohstroh, M., Menard, C., Schulz-Rosengarten, A., Weber, M., Castrillon, J., Lee, E.A.: A language for deterministic coordination across multiple timelines. In: 2020 Forum for Specification and Design Languages (FDL), pp. 1\u20138. IEEE (2020)","DOI":"10.1109\/FDL50818.2020.9232939"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Lohstroh, M., et al.: 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","DOI":"10.1007\/978-3-030-41131-2_4"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Loulou, H., Saudrais, S., Soubra, H., Larouci, C.: Adapting security policy at runtime for connected autonomous vehicles. In: 2016 IEEE 25th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 26\u201331. IEEE (2016)","DOI":"10.1109\/WETICE.2016.16"},{"issue":"4","key":"2_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2542049","volume":"46","author":"R Mitchell","year":"2014","unstructured":"Mitchell, R., Chen, I.R.: A survey of intrusion detection techniques for cyber-physical systems. ACM Comput. Surv. 46(4), 1\u201329 (2014)","journal-title":"ACM Comput. Surv."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Mohan, S., Bak, S., Betti, E., Yun, H., Sha, L., Caccamo, M.: S3a: secure system simplex architecture for enhanced security and robustness of cyber-physical systems. In: Proceedings of the 2nd ACM International Conference on High Confidence Networked Systems, pp. 65\u201374 (2013)","DOI":"10.1145\/2461446.2461456"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-030-58298-2_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Moradi","year":"2020","unstructured":"Moradi, F., Abbaspour Asadollah, S., Sedaghatbaf, A., \u010cau\u0161evi\u0107, A., Sirjani, M., Talcott, C.: An actor-based approach for security analysis of cyber-physical systems. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 130\u2013147. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_5"},{"key":"2_CR29","unstructured":"Ptolemaeus, C.: System design, modeling, and simulation: using Ptolemy II, vol. 1. Ptolemy. org Berkeley (2014)"},{"key":"2_CR30","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)","journal-title":"Sci. Comput. Program."},{"key":"2_CR31","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":"2_CR32","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"},{"issue":"7","key":"2_CR33","doi-asserted-by":"publisher","first-page":"1068","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(7), 1068 (2020)","journal-title":"Mathematics"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Zhang, Q., Li, Z., Seatzu, C., Giua, A.: Stealthy attacks for partially-observed discrete event systems. In: 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), vol. 1, pp. 1161\u20131164. IEEE (2018)","DOI":"10.1109\/ETFA.2018.8502501"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Liu, J., Lee, E.A.: A programming model for time-synchronized distributed real-time systems. In: 13th IEEE Real Time and Embedded Technology and Applications Symposium (RTAS 2007), pp. 259\u2013268. IEEE (2007)","DOI":"10.1109\/RTAS.2007.5"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15077-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,2]],"date-time":"2022-12-02T15:15:44Z","timestamp":1669994144000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15077-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150760","9783031150777"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15077-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"23 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin2022chi.web.illinois.edu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}