{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T16:07:07Z","timestamp":1778947627664,"version":"3.51.4"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Programmable logic controllers (PLCs) are widely used in industrial applications. Ensuring the correctness of PLC programs is important due to their safety-critical nature. Structured text (ST) is an imperative programming language for PLC. Despite recent advances in executable semantics of PLC ST, existing methods neglect complex multitasking and preemption features. This paper presents an executable semantics of PLC\u00a0ST with preemptive multitasking. Formal analysis of multitasking programs experiences the state explosion problem. To mitigate this problem, this paper also proposes state space reduction techniques for model checking multitask PLC ST programs.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_22","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"425-442","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal Semantics and\u00a0Analysis of\u00a0Multitask PLC ST Programs with\u00a0Preemption"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5979-726X","authenticated-orcid":false,"given":"Jaeseo","family":"Lee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"22_CR1","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Bauer, N., et al.: Verification of PLC programs given as sequential function charts. In: Ehrig, H., et al. (eds.) Integration of Software Specification Techniques for Applications in Engineering. LNCS, vol. 3147, pp. 517\u2013540. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27863-4_28","DOI":"10.1007\/978-3-540-27863-4_28"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Bogdanas, D., Ro\u015fu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 445\u2013456. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Bohlender, D., Hamm, D., Kowalewski, S.: Cycle-bounded model checking of PLC software via dynamic large-block encoding. In: Proceedings of the 33rd ACM Symposium on Applied Computing, pp. 1891\u20131898. ACM (2018). https:\/\/doi.org\/10.1145\/3167132.3167334","DOI":"10.1145\/3167132.3167334"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in instruction list. In: Proceedings of the IEEE International Conference on Systems, Man and Cybernetics, vol.\u00a04, pp. 2449\u20132454. IEEE (2000). https:\/\/doi.org\/10.1109\/ICSMC.2000.884359","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"22_CR6","unstructured":"Chikamasa, T.: NXTway-GS C API for a two wheeled self-balancing robot. https:\/\/lejos-osek.sourceforge.net\/nxtway_gs.htm. Accessed 19 Apr 2024"},{"key":"22_CR7","unstructured":"Clarke, Jr., E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. MIT Press (2018)"},{"key":"22_CR8","unstructured":"Clavel, M., et al.: Maude manual (version 3.4). Tech. rep., SRI International, Menlo Park (2024)"},{"key":"22_CR9","unstructured":"Commission, I.E.: Programmable controllers-part 3: programming languages. IEC 61131-3 (1993)"},{"key":"22_CR10","unstructured":"Darvas, D., Blanco\u00a0Vinuela, E., Fern\u00e1ndez\u00a0Adiego, B.: PLCverif: a tool to verify PLC programs based on model checking techniques. In: Proceedings of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems (2015)"},{"issue":"2","key":"22_CR11","doi-asserted-by":"publisher","first-page":"151","DOI":"10.3311\/PPee.9743","volume":"61","author":"D Darvas","year":"2017","unstructured":"Darvas, D., Majzik, I., Vi\u00f1uela, E.B.: PLC program translation for verification purposes. Periodica Polytech. Electric. Eng. Comput. Sci. 61(2), 151\u2013165 (2017). https:\/\/doi.org\/10.3311\/PPee.9743","journal-title":"Periodica Polytech. Electric. Eng. Comput. Sci."},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.\u00a047, pp. 533\u2013544. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Gourcuff, V., De\u00a0Smet, O., Faure, J.M.: Efficient representation for formal verification of PLC programs. In: International Workshop on Discrete Event Systems, pp. 182\u2013187. IEEE (2006). https:\/\/doi.org\/10.1109\/WODES.2006.1678428","DOI":"10.1109\/WODES.2006.1678428"},{"key":"22_CR14","doi-asserted-by":"publisher","unstructured":"Guo, S., Wu, M., Wang, C.: Symbolic execution of programmable logic controller code. In: Proceedings of the Joint Meeting on Foundations of Software Engineering, pp. 326\u2013336. ACM (2017). https:\/\/doi.org\/10.1145\/3106237.3106245","DOI":"10.1145\/3106237.3106245"},{"issue":"15","key":"22_CR15","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 Proceedings Volumes 31(15), 107\u2013112 (1998). https:\/\/doi.org\/10.1016\/S1474-6670(17)40537-4","journal-title":"IFAC Proceedings Volumes"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of C. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, vol.\u00a050, pp. 336\u2013345. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737979","DOI":"10.1145\/2737924.2737979"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al: KEVM: a complete formal semantics of the ethereum virtual machine. In: Proceedings of IEEE Computer Security Foundations Symposium, pp. 204\u2013217. IEEE (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"22_CR18","doi-asserted-by":"publisher","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, 14593\u201314602 (2019). https:\/\/doi.org\/10.1109\/ACCESS.2019.2894026","DOI":"10.1109\/ACCESS.2019.2894026"},{"key":"22_CR19","doi-asserted-by":"publisher","unstructured":"Lamp\u00e9ri\u00e8re-Couffin, S., Lesage, J.J.: Formal Verification of the Sequential Part of PLC Programs, pp. 247\u2013254. Springer (2000). https:\/\/doi.org\/10.1007\/978-1-4615-4493-7_25","DOI":"10.1007\/978-1-4615-4493-7_25"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Lazar, D., et al.: Executing formal semantics with the K tool. In: Proceedings of the International Symposium on Formal Methods. LNCS, vol.\u00a07436, pp. 267\u2013271. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_23","DOI":"10.1007\/978-3-642-32759-9_23"},{"key":"22_CR21","doi-asserted-by":"publisher","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(6), 911\u2013948 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00665-z","DOI":"10.1007\/s10009-022-00665-z"},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: International Conference on Computer Aided Verification, pp. 491\u2013504. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23","DOI":"10.1007\/978-3-030-81685-8_23"},{"key":"22_CR23","unstructured":"Lee, J., Bae, K.: Supplementary materials and technical report (2024). https:\/\/github.com\/postechsv\/plc-release\/releases\/tag\/v1.1"},{"key":"22_CR24","doi-asserted-by":"publisher","unstructured":"Lee, J., Kim, S., Bae, K.: Bounded model checking of PLC ST programs using rewriting modulo SMT. In: Proceedings of the ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, pp. 56\u201367. ACM (2022). https:\/\/doi.org\/10.1145\/3563822.3568016","DOI":"10.1145\/3563822.3568016"},{"key":"22_CR25","unstructured":"Li, J., Qeriqi, A., Steffen, M., Yu, I.C.: Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems. In: Proceedings of the Norsk Informatikkonferanse. Bibsys Open Journal Systems, Norway (2016). https:\/\/dblp.org\/rec\/conf\/nik\/LiQSY16.html"},{"issue":"4","key":"22_CR26","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1474-6670(17)36116-5","volume":"37","author":"A Lobov","year":"2004","unstructured":"Lobov, A., Lastra, J.L.M., Tuokko, R., Vyatkin, V.: Modelling and verification of PLC-based systems programmed with ladder diagrams. IFAC Proceedings Volumes 37(4), 183\u2013188 (2004). https:\/\/doi.org\/10.1016\/S1474-6670(17)36116-5","journal-title":"IFAC Proceedings Volumes"},{"issue":"1","key":"22_CR27","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). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"22_CR28","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1109\/TASE.2010.2050199","volume":"7","author":"HB Mokadem","year":"2010","unstructured":"Mokadem, H.B., Berard, B., Gourcuff, V., De Smet, O., Roussel, J.M.: Verification of a timed multitask system with Uppaal. IEEE Trans. Autom. Sci. Eng. 7(4), 921\u2013932 (2010). https:\/\/doi.org\/10.1109\/TASE.2010.2050199","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"4","key":"22_CR29","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). https:\/\/doi.org\/10.1016\/j.entcs.2007.06.005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"22_CR30","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. High. Order Symbol. Comput. 20, 161\u2013196 (2007)","journal-title":"High. Order Symbol. Comput."},{"key":"22_CR31","doi-asserted-by":"publisher","unstructured":"Park, D., Stef\u0103nescu, A., Ro\u015fu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 346\u2013356. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"key":"22_CR32","doi-asserted-by":"publisher","unstructured":"Pavlovic, O., Ehrich, H.D.: Model checking PLC software written in function block diagram. In: Proceedings of the International Conference on Software Testing, Verification and Validation, pp. 439\u2013448. IEEE (2010). https:\/\/doi.org\/10.1109\/ICST.2010.10","DOI":"10.1109\/ICST.2010.10"},{"key":"22_CR33","doi-asserted-by":"publisher","unstructured":"Peled, D.: Handbook of Model Checking, pp. 173\u2013190. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"22_CR34","doi-asserted-by":"publisher","unstructured":"Rausch, M., Krogh, B.H.: Formal verification of PLC programs. In: Proceedings of the American Control Conference, vol.\u00a01, pp. 234\u2013238. IEEE (1998). https:\/\/doi.org\/10.1109\/ACC.1998.694666","DOI":"10.1109\/ACC.1998.694666"},{"issue":"6","key":"22_CR35","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. Logic Algeb. Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","journal-title":"J. Logic Algeb. Program."},{"key":"22_CR36","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.entcs.2014.05.002","DOI":"10.1016\/j.entcs.2014.05.002"},{"key":"22_CR37","doi-asserted-by":"publisher","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: International Workshop on Rewriting Logic and its Applications, pp. 104\u2013122. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_8","DOI":"10.1007\/978-3-642-16310-4_8"},{"issue":"10","key":"22_CR38","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. Softw. Eng. 49(10), 4796\u20134813 (2023). https:\/\/doi.org\/10.1109\/TSE.2023.3315292","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:06:51Z","timestamp":1725934011000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}