{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:42:20Z","timestamp":1767984140902,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-10794-7_9","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:29Z","timestamp":1763189009000},"page":"162-181","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Online Model Checking for\u00a0Anomaly Detection in\u00a0Industrial Control Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5291-6519","authenticated-orcid":false,"given":"Douglas","family":"Fraser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0941-1717","authenticated-orcid":false,"given":"Alice","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5232-2381","authenticated-orcid":false,"given":"Marco","family":"Cook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0939-378X","authenticated-orcid":false,"given":"Dimitrios","family":"Pezaros","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Adiego, B.F., Darvas, D., Tournier, J.C., Vi\u00f1uela, E.B., Su\u00e1rez, V.M.G.: Bringing automated model checking to PLC program development \u2013 a CERN case study \u2013. IFAC Proc. Volumes 47(2), 394\u2013399 (2014)","DOI":"10.3182\/20140514-3-FR-4046.00051"},{"key":"9_CR2","unstructured":"AG, S.: S7 communication with PUT\/GET. Tech. rep., Siemens AG (2020)"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.jnca.2015.11.016","volume":"60","author":"M Ahmed","year":"2016","unstructured":"Ahmed, M., Naser Mahmood, A., Hu, J.: A survey of network anomaly detection techniques. J. Netw. Comput. Appl. 60, 19\u201331 (2016)","journal-title":"J. Netw. Comput. Appl."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Akers: binary decision diagrams. IEEE Trans. Comput. 100(6), 509\u2013516 (1978)","DOI":"10.1109\/TC.1978.1675141"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: QEST, vol.\u00a06, pp. 125\u2013126. Citeseer (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Berthier, R., Sanders, W.H.: Specification-based intrusion detection for advanced metering infrastructures, pp. 184\u2013193 (2011). https:\/\/doi.org\/10.1109\/PRDC.2011.30, https:\/\/www.scopus.com\/inward\/record.uri?eid=2-s2.0-84857771025&doi=10.1109%2fPRDC.2011.30 &partnerID=40 &md5=9973d92c8fafc0c467bbba326250508a","DOI":"10.1109\/PRDC.2011.30"},{"key":"9_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2019.101677","volume":"89","author":"D Bhamare","year":"2020","unstructured":"Bhamare, D., Zolanvari, M., Erbad, A., Jain, R., Khan, K., Meskin, N.: Cybersecurity for industrial control systems: a survey. Comput. Secur. 89, 101677 (2020)","journal-title":"Comput. Secur."},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Chandola, V., Banerjee, A., Kumar, V.: Anomaly detection: a survey. ACM Comput. Surv. 41(3) (2009). https:\/\/doi.org\/10.1145\/1541880.1541882","DOI":"10.1145\/1541880.1541882"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Chauhan, H., Kumar, V., Pundir, S., Pilli, E.S.: A comparative study of classification techniques for intrusion detection. In: 2013 International Symposium on Computational and Business Intelligence, pp. 40\u201343. IEEE (2013)","DOI":"10.1109\/ISCBI.2013.16"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Cimatti, A., et al.: NuSMV 2: An OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cook, M., Marnerides, A., Johnson, C., Pezaros, D.: A survey on industrial control system digital forensics: challenges, advances and future directions. IEEE Commun. Surv. Tutorials 25(3), 1705\u20131747 (2023)","DOI":"10.1109\/COMST.2023.3264680"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Cook, M.M., Marnerides, A.K., Pezaros, D.: Plcprint: Fingerprinting memory attacks in programmable logic controllers. IEEE Trans. Inf. Forensics Secur. 18, 3376\u20133387 (2023)","DOI":"10.1109\/TIFS.2023.3277688"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Darvas, D., Blanco\u00a0Vinuela, E., Fern\u00e1ndez\u00a0Adiego, B.: PLCverif: a tool to verify PLC programs based on model checking techniques, p. WEPGF092 (2015).https:\/\/doi.org\/10.18429\/JACoW-ICALEPCS2015-WEPGF092, https:\/\/cds.cern.ch\/record\/2213507","DOI":"10.18429\/JACoW-ICALEPCS2015-WEPGF092"},{"key":"9_CR14","unstructured":"Gerth, R.: Concise promela reference (1997). https:\/\/spinroot.com\/spin\/Man\/Quick.html. Accessed 8 Jan 2024"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Hailesellasie, M., Hasan, S.R.: Intrusion detection in plc-based industrial control systems using formal verification approach in conjunction with graphs. J. Hardware Syst. Secur. 2, 1\u201314 (2018)","DOI":"10.1007\/s41635-017-0017-y"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Han, S., Xie, M., Chen, H.H., Ling, Y.: Intrusion detection in cyber-physical systems: techniques and challenges. IEEE Syst. J. 8(4), 1052\u20131062 (2014). https:\/\/doi.org\/10.1109\/JSYST.2013.2257594","DOI":"10.1109\/JSYST.2013.2257594"},{"key":"9_CR17","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 1st edn. (2011)"},{"key":"9_CR18","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, vol.\u00a01003. Addison-Wesley Reading (2004)"},{"key":"9_CR19","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-0-387-34878-0_13","volume-title":"Formal Description Techniques VII","author":"GJ Holzmann","year":"1995","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Formal Description Techniques VII. IAICT, pp. 197\u2013211. Springer, Boston, MA (1995). https:\/\/doi.org\/10.1007\/978-0-387-34878-0_13"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Hotellier, E., Sicard, F., Francq, J., Mocanu, S.: Standard specification-based intrusion detection for hierarchical industrial control systems. Inf. Sci. 659, 120102 (2024)","DOI":"10.1016\/j.ins.2024.120102"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Khairullah, S.S.: Formal verification of a dependable state machine-based hardware architecture for safety-critical cyber-physical systems: analysis, design, and implementation. J. Electron. Test. 40(4), 509\u2013523 (2024)","DOI":"10.1007\/s10836-024-06126-6"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Kottler, S., Khayamy, M., Hasan, S.R., Elkeelany, O.: Formal verification of ladder logic programs using NUSMV. In: SoutheastCon 2017, pp.\u00a01\u20135 (2017). https:\/\/doi.org\/10.1109\/SECON.2017.7925390","DOI":"10.1109\/SECON.2017.7925390"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Liao, H.J., Richard Lin, C.H., Lin, Y.C., Tung, K.Y.: Intrusion detection system: a comprehensive review. J. Netw. Comput. Appl. 36(1), 16\u201324 (2013)","DOI":"10.1016\/j.jnca.2012.09.004"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Miller, A., Porr, B., Valkov, I., Fraser, D., Pagojus, D.: Model checking with memoisation for fast overtaking planning. Sci. Comput. Program. 244, 103300 (2025)","DOI":"10.1016\/j.scico.2025.103300"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Miller, T., Staves, A., Maesschalck, S., Sturdee, M., Green, B.: Looking back to look forward: Lessons learnt from cyber-attacks on industrial control systems. Int. J. Crit. Infrastruct. Prot. 35, 100464 (2021)","DOI":"10.1016\/j.ijcip.2021.100464"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Mitchell, R., Chen, I.R.: A survey of intrusion detection techniques for cyber-physical systems. ACM Comput. Surv. 46(4) (2014). https:\/\/doi.org\/10.1145\/2542049","DOI":"10.1145\/2542049"},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Mitchell, R., Chen, I.R.: Behavior rule specification-based intrusion detection for safety critical medical cyber physical systems. IEEE Trans. Dependable Secure Comput. 12(1), 16\u201330 (2015). https:\/\/doi.org\/10.1109\/TDSC.2014.2312327","DOI":"10.1109\/TDSC.2014.2312327"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Nweke, L.O.: A survey of specification-based intrusion detection techniques for cyber-physical systems (2021)","DOI":"10.14569\/IJACSA.2021.0120506"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Rehman, S., Al-Hadhrami, L.M., Alam, M.M.: Pumped hydro energy storage system: a technological review. Renew. Sustain. Energy Rev. 44, 586\u2013598 (2015)","DOI":"10.1016\/j.rser.2014.12.040"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Sakata, K., Fujita, S., Sawada, K., Iwasawa, H., Endoh, H., Matsumoto, N.: Model verification of fallback control system under cyberattacks via UPPAAL. Adv. Robot. 37(3), 156\u2013168 (2D023)","DOI":"10.1080\/01691864.2022.2134737"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Shrestha, R., Mehrpouyan, H., Xu, D.: Model checking of security properties in industrial control systems (ICS). In: Proceedings of the Eighth ACM Conference on Data and Application Security and Privacy, pp. 164\u2013166. CODASPY 2018, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3176258.3176949","DOI":"10.1145\/3176258.3176949"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Song, T., Ko, C., Tseng, C.H., Balasubramanyam, P., Chaudhary, A., Levitt, K.N.: Formal reasoning about a specification-based intrusion detection for dynamic auto-configuration protocols in ad hoc networks. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) Formal Aspects in Security and Trust: Thrid International Workshop, FAST 2005, Newcastle upon Tyne, UK, 18-19 July 2005, Revised Selected Papers, pp. 16\u201333. Springer (2006). https:\/\/doi.org\/10.1007\/11679219_3","DOI":"10.1007\/11679219_3"},{"issue":"1","key":"9_CR34","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s10462-021-10037-9","volume":"55","author":"A Thakkar","year":"2022","unstructured":"Thakkar, A., Lohiya, R.: A survey on intrusion detection system: feature selection, model, performance measures, application perspective, challenges, and future research directions. Artif. Intell. Rev. 55(1), 453\u2013563 (2022)","journal-title":"Artif. Intell. Rev."},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Tournier, J.C., Fern\u00e1ndez\u00a0Adiego, B., Lopez-Miguel, I.D.: PLCverif: status of a formal verification tool for programmable logic controller. In: Proceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems ICALEPCS2021, China (2022).https:\/\/doi.org\/10.18429\/JACOW-ICALEPCS2021-MOPV042, https:\/\/jacow.org\/icalepcs2021\/doi\/JACoW-ICALEPCS2021-MOPV042.html","DOI":"10.18429\/JACOW-ICALEPCS2021-MOPV042"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Uppuluri, P., Sekar, R.: Experiences with specification-based intrusion detection. In: Lee, W., M\u00e9, L., Wespi, A. (eds.) International Workshop on Recent Advances in Intrusion Detection, pp. 172\u2013189. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45474-8_11","DOI":"10.1007\/3-540-45474-8_11"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Wang, T., Su, Q., Chen, T.: Formal analysis of security properties of cyber-physical system based on timed automata. In: 2017 IEEE Second International Conference on Data Science in Cyberspace (DSC), pp. 534\u2013540. IEEE (2017)","DOI":"10.1109\/DSC.2017.44"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Wardak, H., Zhioua, S., Almulhem, A.: PLC access control: a security analysis. In: 2016 World Congress on Industrial Control Systems Security (WCICSS), pp.\u00a01\u20136 (2016). https:\/\/doi.org\/10.1109\/WCICSS.2016.7882935","DOI":"10.1109\/WCICSS.2016.7882935"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:49Z","timestamp":1767967189000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}