{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T04:48:46Z","timestamp":1780462126779,"version":"3.54.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032071057","type":"print"},{"value":"9783032071064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"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-07106-4_14","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:38:17Z","timestamp":1759847897000},"page":"328-356","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Analysis of\u00a0Networked PLC Controllers Interacting with\u00a0Physical Environments"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5979-726X","authenticated-orcid":false,"given":"Jaeseo","family":"Lee","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,6]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Aires\u00a0Urquiza, A., et al.: Resource-bounded intruders in denial of service attacks. In: CSF 2019, pp. 382\u2013396. IEEE (2019)","DOI":"10.1109\/CSF.2019.00033"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Antonioli, D., Tippenhauer, N.O.: MiniCPS: a toolkit for security research on CPS networks. In: CPS-SPC, pp. 91\u2013100. ACM (2015)","DOI":"10.1145\/2808705.2808715"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: HSCC. ACM (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","volume":"178","author":"K Bae","year":"2019","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20\u201342 (2019)","journal-title":"Sci. Comput. Program."},{"key":"14_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bogdanas, D., Ro\u015fu, G.: K-Java: A complete semantics of Java. In: POPL, pp. 445\u2013456. ACM (2015)","DOI":"10.1145\/2676726.2676982"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Bohlender, D., Hamm, D., Kowalewski, S.: Cycle-bounded model checking of PLC software via dynamic large-block encoding. In: SAC, pp. 1891\u20131898. ACM (2018)","DOI":"10.1145\/3167132.3167334"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in Instruction List. In: SMC, vol.\u00a04, pp. 2449\u20132454. IEEE (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"14_CR9","unstructured":"Clavel, M., et al.: Maude manual (version 3.5.1) (2025)"},{"key":"14_CR10","unstructured":"Clavel, M., et al.: All About Maude \u2013 A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"14_CR11","unstructured":"Darvas, D., Blanco\u00a0Vinuela, E., Fern\u00e1ndez\u00a0Adiego, B.: PLCverif: a tool to verify PLC programs based on model checking techniques. In: Accelerator and Large Experimental Physics Control Systems (2015)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Darvas, D., Majzik, I., Vi\u00f1uela, E.B.: PLC program translation for verification purposes. Period. Polytech. Elec. Eng. and Comput. Sci. 61(2), 151\u2013165 (2017)","DOI":"10.3311\/PPee.9743"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, vol.\u00a047, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Ghanaim, A., Frey, G.: Modeling and control of closed-loop networked PLC-systems. In: ACC, pp. 502\u2013508. IEEE (2011)","DOI":"10.1109\/ACC.2011.5991287"},{"issue":"15","key":"14_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S1474-6670(17)40537-4","volume":"31","author":"G Hassapis","year":"1998","unstructured":"Hassapis, G., Kotini, I., Doulgeri, Z.: Validation of a SFC software specification by using hybrid automata. IFAC Proc. Vol. 31(15), 107\u2013112 (1998)","journal-title":"IFAC Proc. Vol."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Huang, Y., Bu, X., Zhu, G., Ye, X., Zhu, X., Shi, J.: KST: executable formal semantics of IEC 61131-3 structured text for verification. IEEE Access 7 (2019)","DOI":"10.1109\/ACCESS.2019.2894026"},{"key":"14_CR18","unstructured":"International Electrotechnical Commission: Programmable controllers - part 3: Programming languages. IEC 61131-3 (1993)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Lamp\u00e9ri\u00e8re-Couffin, S., Lesage, J.J.: Formal verification of the sequential part of PLC programs. In: Discrete Event Systems: Analysis and Control. SECS, vol.\u00a0569, pp. 247\u2013254. Springer (2000)","DOI":"10.1007\/978-1-4615-4493-7_25"},{"key":"14_CR20","unstructured":"Lanotte, R., Merro, M., Munteanu, A., et\u00a0al.: A process calculus approach to correctness enforcement of PLCs. In: CEUR Workshop Proceedings, vol.\u00a02756 (2020)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Lazar, D., et al.: Executing formal semantics with the K tool. In: FM. LNCS, vol.\u00a07436, pp. 267\u2013271. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-32759-9_23"},{"key":"14_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-022-00665-z","volume":"24","author":"J Lee","year":"2022","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C., Kim, S., Kang, M.: Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. Int. J. Softw. Tools Technol. Transf. 24, 1\u201338 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-81685-8_23","volume-title":"Computer Aided Verification","author":"J Lee","year":"2021","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: Hybrid SynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 491\u2013504. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K.: Formal analysis of networked PLC controllers interacting with physical environments (2025). https:\/\/arxiv.org\/abs\/2507.15596","DOI":"10.1007\/978-3-032-07106-4_14"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K.: Formal semantics and analysis of multitask PLC ST programs with preemption. In: Formal Methods. LNCS, vol. 14933, pp. 425\u2013442. Springer, Cham (2025)","DOI":"10.1007\/978-3-031-71162-6_22"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K.: Bounded model checking of PLC ST programs using rewriting modulo SMT. In: FTSCS, pp. 56\u201367. ACM (2022)","DOI":"10.1145\/3563822.3568016"},{"issue":"7\u20138","key":"14_CR27","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Logic Algebraic Program."},{"issue":"1","key":"14_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"14_CR29","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1007\/s10796-016-9671-9","volume":"18","author":"J Nellen","year":"2016","unstructured":"Nellen, J., Driessen, K., Neuh\u00e4u\u00dfer, M.R., \u00c1brah\u00e1m, E., Wolters, B.: Two CEGAR-based approaches for the safety verification of PLC-controlled plants. Inf. Syst. Front. 18(5), 927\u2013952 (2016)","journal-title":"Inf. Syst. Front."},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Nigam, V., Talcott, C.: Automating safety proofs about cyber-physical systems using rewriting modulo SMT. In: WRLA. LNCS, vol. 13252. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-12441-9_11"},{"issue":"4","key":"14_CR31","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2007.06.005","volume":"176","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for real-time maude. Electron. Notes Theor. Comput. Sci. 176(4), 5\u201327 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"14_CR32","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time maude. Higher-Order Symb. Comput. 20, 161\u2013196 (2007)","journal-title":"Higher-Order Symb. Comput."},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Park, D., Stef\u0103nescu, A., Ro\u015fu, G.: KJS: a complete formal semantics of JavaScript. In: PLDI, pp. 346\u2013356. ACM (2015)","DOI":"10.1145\/2737924.2737991"},{"key":"14_CR34","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-10575-8_6","volume-title":"Handbook of Model Checking","author":"D Peled","year":"2018","unstructured":"Peled, D.: Partial-order reduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 173\u2013190. Springer, Cham (2018)"},{"issue":"1","key":"14_CR35","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Logical Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Logical Algebraic Methods Program."},{"issue":"6","key":"14_CR36","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Rosu","year":"2010","unstructured":"Rosu, G., Serb\u0103nut\u0103, T.F.: An overview of the K semantic framework. J. Log. Algebr. Methods Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"14_CR37","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2014.05.002","volume":"304","author":"G Ro\u015fu","year":"2014","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: K overview and simple case study. Electron. Notes Theor. Comput. Sci. 304, 3\u201356 (2014)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"14_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-16310-4_8","volume-title":"Rewriting Logic and Its Applications","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2010","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 104\u2013122. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_8"},{"issue":"10","key":"14_CR39","doi-asserted-by":"publisher","first-page":"4796","DOI":"10.1109\/TSE.2023.3315292","volume":"49","author":"K Wang","year":"2023","unstructured":"Wang, K., Wang, J., Poskitt, C.M., Chen, X., Sun, J., Cheng, P.: K-ST: a formal executable semantics of the structured text language for PLCs. IEEE Trans. Software Eng. 49(10), 4796\u20134813 (2023)","journal-title":"IEEE Trans. Software Eng."},{"key":"14_CR40","doi-asserted-by":"crossref","unstructured":"Yu, G., Bae, K.: A flexible framework for integrating Maude and SMT solvers using Python. In: WRLA. LNCS, vol. 14953, pp. 179\u2013192. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65941-6_10"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07106-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T22:02:58Z","timestamp":1760047378000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07106-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,6]]},"ISBN":["9783032071057","9783032071064"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07106-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,6]]},"assertion":[{"value":"6 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","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":"13 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2025.splashcon.org\/home\/sas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}