{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T17:14:46Z","timestamp":1769879686615,"version":"3.49.0"},"reference-count":62,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"publisher","award":["2020YFB2010900"],"award-info":[{"award-number":["2020YFB2010900"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"publisher","award":["61833015"],"award-info":[{"award-number":["61833015"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"publisher","award":["62293511"],"award-info":[{"award-number":["62293511"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100022963","name":"Provincial Key R&D Program of Zhejiang","doi-asserted-by":"publisher","award":["2020C01038"],"award-info":[{"award-number":["2020C01038"]}],"id":[{"id":"10.13039\/100022963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100022963","name":"Provincial Key R&D Program of Zhejiang","doi-asserted-by":"publisher","award":["2021C01032"],"award-info":[{"award-number":["2021C01032"]}],"id":[{"id":"10.13039\/100022963","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Starry Night Science Fund of Zhejiang University Shanghai Institute for Advanced Study","award":["SN-ZJU-SIAS-001"],"award-info":[{"award-number":["SN-ZJU-SIAS-001"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2023,10,1]]},"DOI":"10.1109\/tse.2023.3315292","type":"journal-article","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T17:50:40Z","timestamp":1694713840000},"page":"4796-4813","source":"Crossref","is-referenced-by-count":7,"title":["K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs"],"prefix":"10.1109","volume":"49","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5523-1330","authenticated-orcid":false,"given":"Kun","family":"Wang","sequence":"first","affiliation":[{"name":"College of Control Science and Engineering, Zhejiang University, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7113-7635","authenticated-orcid":false,"given":"Jingyi","family":"Wang","sequence":"additional","affiliation":[{"name":"College of Control Science and Engineering, Zhejiang University, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9376-2471","authenticated-orcid":false,"given":"Christopher M.","family":"Poskitt","sequence":"additional","affiliation":[{"name":"School of Computing and Information Systems, Singapore Management University, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4482-3430","authenticated-orcid":false,"given":"Xiangxiang","family":"Chen","sequence":"additional","affiliation":[{"name":"College of Control Science and Engineering, Zhejiang University, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"School of Computing and Information Systems, Singapore Management University, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4453-2274","authenticated-orcid":false,"given":"Peng","family":"Cheng","sequence":"additional","affiliation":[{"name":"College of Control Science and Engineering, Zhejiang University, Zhejiang, China"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2011.67"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TPWRS.2016.2631891"},{"key":"ref3","article-title":"The Ukrainian power grid was hacked again","author":"Zetter","year":"2017","journal-title":"Motherboard"},{"key":"ref4","article-title":"A cyberattack in Saudi Arabia had a deadly goal. Experts fear another try","author":"Perlroth","year":"2018"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ICECS.2018.8618042"},{"key":"ref6","article-title":"Security research: CODESYS runtime, a PLC control framework","author":"Nochvay","year":"2019","journal-title":"Kaspersky ICS CERT"},{"key":"ref7","first-page":"2847","article-title":"ICSFuzz: Manipulating I\/Os and repurposing binary code to enable instrumented fuzzing in ICS control applications","volume-title":"Proc. 30th USENIX Secur. Symp. (USENIX Security)","author":"Tychalas","year":"2021"},{"key":"ref8","volume-title":"Programmable Controllers\u2014Part 3: Programming Languages","year":"2013"},{"key":"ref9","volume-title":"PLC Controls With Structured Text (ST), V3: IEC 61131-3 and Best Practice ST Programming","author":"Antonsen","year":"2020"},{"key":"ref10","article-title":"On formal reasoning on the semantics of PLC using Coq","author":"Blech","year":"2013"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_6"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0448-7"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.3390\/electronics4040995"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/RWEEK.2016.7573309"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_18"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_32"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23313"},{"key":"ref18","first-page":"1","article-title":"PLC-Blaster: A worm living solely in the PLC","volume":"16","author":"Spenneberg","year":"2016","journal-title":"Black Hat Asia"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23271"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106245"},{"key":"ref21","article-title":"A trusted safety verifier for process controller code,\u201d","volume":"14","author":"McLaughlin","year":"2014","journal-title":"Proc. NDSS"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2020.2999716"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00034"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27863-4_28"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.1999.777456"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2001.972974"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.026"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.2478\/v10233-011-0031-3"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.3182\/20140824-6-ZA-1003.01279"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/ICCSSE.1996.554845"},{"key":"ref32","volume-title":"Petri net semantics for the PLC user programming language Instruction List","author":"Heiner","year":"1997"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594334"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3363562"},{"issue":"1","key":"ref36","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"McKeeman","year":"1998","journal-title":"Digit. Tech. J."},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_14"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2894026"},{"key":"ref39","first-page":"186","article-title":"K: A semantic framework for programming languages and formal analysis tools","volume":"50","author":"Rosu","year":"2017","journal-title":"Dependable Softw. Syst. Eng."},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.2514\/1.I010699"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3360581"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/GHTC.2014.6970342"},{"key":"ref43","first-page":"6","article-title":"Generic representation of PLC programming languages for formal verification","volume-title":"Proc. 23rd PhD Mini-Symp","author":"Darvas","year":"2016"},{"key":"ref44","first-page":"20","article-title":"Programming PLCs using structured text","volume-title":"Proc. Int. Multiconf. Comput. Sci. Inf. Technol","author":"Roos","year":"2008"},{"key":"ref45","article-title":"Automated test generation for structured text language using uppaal model checker","author":"Markovic","year":"2015"},{"key":"ref46","volume-title":"IEC 61131-3: Programming Industrial Automation Systems","author":"Tiegelkamp","year":"2010"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00357-7"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984027"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103719"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2018.00014"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00066"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0_7"},{"key":"ref55","first-page":"129","article-title":"Backus-Naur Form (BNF)","volume-title":"Encyclopedia of Computer Science","author":"McCracken","year":"2003"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.05.002"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/TMPA.2013.7163716"},{"key":"ref58","first-page":"907","article-title":"A formal specification method for PLC-based applications","volume-title":"Proc. 15th Int. Conf. Accel. Large Exp. Phys. Control Syst. (ICALEPCS 2015)","author":"Darvas","year":"2015"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2489184"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1007\/s41635-017-0017-y"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.06.336"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1016\/j.compchemeng.2017.11.004"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/10286436\/10251676.pdf?arnumber=10251676","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T05:45:36Z","timestamp":1716443136000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10251676\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,1]]},"references-count":62,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tse.2023.3315292","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,1]]}}}