{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T04:47:27Z","timestamp":1761367647669,"version":"build-2065373602"},"reference-count":61,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"National Natural Science Foundation of China (NSFC) General Program","award":["62273305"],"award-info":[{"award-number":["62273305"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans.Inform.Forensic Secur."],"published-print":{"date-parts":[[2025]]},"DOI":"10.1109\/tifs.2025.3620682","type":"journal-article","created":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T17:39:59Z","timestamp":1760377199000},"page":"1-1","source":"Crossref","is-referenced-by-count":0,"title":["Verifying PLC Control Logic for Physical Module Integrity Guided by Wiring Diagrams"],"prefix":"10.1109","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5788-7281","authenticated-orcid":false,"given":"Chengtao","family":"Yao","sequence":"first","affiliation":[{"name":"College of Control Science and Engineering, State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6816-6459","authenticated-orcid":false,"given":"Chengcheng","family":"Zhao","sequence":"additional","affiliation":[{"name":"College of Control Science and Engineering, State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1596-6890","authenticated-orcid":false,"given":"Zeyu","family":"Yang","sequence":"additional","affiliation":[{"name":"iTrust, Singapore University of Technology and Design, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4221-2162","authenticated-orcid":false,"given":"Peng","family":"Cheng","sequence":"additional","affiliation":[{"name":"College of Control Science and Engineering, State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3155-3145","authenticated-orcid":false,"given":"Jiming","family":"Chen","sequence":"additional","affiliation":[{"name":"College of Control Science and Engineering, State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382244"},{"key":"ref2","first-page":"1","article-title":"Internet-facing PLCs\u2014A new back orifice","volume-title":"Black Hat USA","author":"Klick","year":"Aug. 2015"},{"key":"ref3","first-page":"1","article-title":"PLC-blaster: A worm living solely in the PLC","author":"Spenneberg","year":"Mar. 2016","journal-title":"Black Hat Asia"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.14722\/bar.2019.23074"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/IECON48115.2021.9589721"},{"issue":"6","key":"ref6","first-page":"29","article-title":"W32. Stuxnet dossier","volume":"5","author":"Falliere","year":"2011"},{"volume-title":"How Does Triton Attack Triconex Industrial Safety Systems?","year":"2021","author":"Lab","key":"ref7"},{"volume-title":"Throwback Attack: Hackers Attempt to Flood Israeli Water Supply With Chlorine","year":"2022","author":"WALL","key":"ref8"},{"volume-title":"Detailed Explanation of Motor Forward and Reverse Circuit and Common Faults","year":"2024","key":"ref9"},{"volume-title":"Principles of Model Checking","year":"2008","author":"Baier","key":"ref10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23043"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.5220\/0006418705670574"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/SECON.2017.7925390"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00018-9_22"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/FDL.2014.7119356"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2489184"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_32"},{"key":"ref18","first-page":"1677","article-title":"Formal consistency checking over specifications in natural languages","volume-title":"Proc. Design, Autom. Test Eur. Conf. Exhib. (DATE)","author":"Yan"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-77474-5_11"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_4"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00034"},{"author":"Moln\u00e1r","key":"ref23","article-title":"PLCverif re-engineered: An open platform for the formal analysis of PLC programs"},{"article-title":"DRAFT PLC programming for industrial automation","year":"2014","author":"Collins","key":"ref24"},{"volume-title":"How to Read a PLC Wiring Diagram?","year":"2024","key":"ref25"},{"volume-title":"Bottle Filling PLC Ladder Logic","key":"ref26"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2018.05.034"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1520\/SSMS20170006"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.proeng.2011.08.025"},{"issue":"7","key":"ref30","first-page":"103","article-title":"PLC based object sorting automation","volume":"3","author":"Bargal","year":"2016","journal-title":"Int. Res. J. Eng. Technol. (IRJET)"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.4236\/oalib.1105891"},{"volume-title":"Traffic Light Control Using PLC Ladder Logic Programming","year":"2024","key":"ref32"},{"volume-title":"PLC Automatic Car Washing System Project","key":"ref33"},{"issue":"1","key":"ref34","first-page":"3","article-title":"Analysis of the cyber attack on the Ukrainian power grid","volume":"388","author":"Case","year":"2016","journal-title":"Electr. Inf. Sharing Anal. Center"},{"volume-title":"ICS ADVISORY: Rockwell Automation Logix Controllers","key":"ref35"},{"volume-title":"CVE-2021-22681: Authentication Bypass Vulnerability Found in Logix Controllers","year":"2021","key":"ref36"},{"volume-title":"SSA-568427: Weak Key Protection Vulnerability in SIMATIC S7-1200 and S7-1500 CPU Families","year":"2022","key":"ref37"},{"article-title":"Malicious control system cyber security attack case study-maroochy water services, Australia","year":"2008","author":"Abrams","key":"ref38"},{"key":"ref39","first-page":"81","article-title":"PLC security and critical infrastructure protection","volume-title":"Proc. IEEE 8th Int. Conf. Ind. Inf. Syst.","author":"Sandaruwan","year":"2024"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/SPW53761.2021.00058"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.3390\/electronics8080825"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1016\/j.neunet.2020.05.025"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/ICDI57181.2022.10007281"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TPAMI.2008.300"},{"key":"ref45","first-page":"248","article-title":"PLCverif: Status of a formal verification tool for programmable logic controller","volume":"2022","author":"Lopez-Miguel","year":"2022","journal-title":"JACoW"},{"volume-title":"Transforming PLC programs into formal models for verification purposes","year":"2013","author":"Darvas","key":"ref46"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.3182\/20140824-6-ZA-1003.01279"},{"volume-title":"IEC Symbol Preview","year":"2024","key":"ref48"},{"volume-title":"Natural Language Processing With Python and SpaCy: A Practical Introduction","year":"2020","author":"Vasiliev","key":"ref49"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.acl-demos.14"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-021-00312-y"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.3311\/ppee.9743"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9415-7"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1016\/j.compchemeng.2017.11.004"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351741"},{"article-title":"PLCverif: A tool to verify PLC programs based on model checking techniques","year":"2015","author":"Darvas","key":"ref57"},{"volume-title":"Automated verification of programmable logic controller programs against structured natural language requirements","year":"2023","author":"\u00c1d\u00e1m","key":"ref58"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.3390\/electronics9040572"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_18"},{"key":"ref61","article-title":"Applying model checking to highly-configurable safety critical software: The SPS-PPS PLC program","author":"Fernandez Adiego","year":"2022","journal-title":"arXiv:2203.16148"}],"container-title":["IEEE Transactions on Information Forensics and Security"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10206\/4358835\/11202252.pdf?arnumber=11202252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T04:43:32Z","timestamp":1761367412000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11202252\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":61,"URL":"https:\/\/doi.org\/10.1109\/tifs.2025.3620682","relation":{},"ISSN":["1556-6013","1556-6021"],"issn-type":[{"type":"print","value":"1556-6013"},{"type":"electronic","value":"1556-6021"}],"subject":[],"published":{"date-parts":[[2025]]}}}