{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,22]],"date-time":"2026-07-22T16:04:14Z","timestamp":1784736254099,"version":"3.55.0"},"reference-count":56,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"Space Optoelectronic Measurement and Perception Lab, Beijing Institute of Control Engineering","award":["LabSOMP-2023-03"],"award-info":[{"award-number":["LabSOMP-2023-03"]}]},{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"publisher","award":["62172299"],"award-info":[{"award-number":["62172299"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"publisher","award":["62032019"],"award-info":[{"award-number":["62032019"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Syst. Man Cybern, Syst."],"published-print":{"date-parts":[[2025,10]]},"DOI":"10.1109\/tsmc.2025.3585039","type":"journal-article","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T18:06:16Z","timestamp":1753207576000},"page":"7410-7424","source":"Crossref","is-referenced-by-count":1,"title":["An Innovative Formal Verification Method Based on Timed Petri Nets With Integrated Database Tables"],"prefix":"10.1109","volume":"55","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2958-7509","authenticated-orcid":false,"given":"Jian","family":"Song","sequence":"first","affiliation":[{"name":"School of Computer Science and Technology, Tongji University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7523-4827","authenticated-orcid":false,"given":"Guanjun","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, Tongji University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6064-1908","authenticated-orcid":false,"given":"Ying","family":"Tang","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Rowan University, Glassboro, NJ, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li","family":"Wang","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Miaomiao","family":"Wang","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lin","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2023.119922"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2020.3046673"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2021.3122428"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2021.3118655"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TCSS.2021.3132355"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2025.3545756"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1082983.1083249"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.3390\/s150304837"},{"key":"ref9","volume-title":"Cyber-Physical Systems: Foundations, Principles and Applications","author":"Song","year":"2016"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2023.3243558"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-13050-3_4"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2017.2778077"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2001858.2002085"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503503"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_19"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2022.3163741"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2022.3173170"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2023.3246057"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2024.3397695"},{"key":"ref20","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3570326"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2024.3509901"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0161-4"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2022.3181669"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-19-6309-4"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2016.11.011"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2022.3195869"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/WiCOM.2012.6478590"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(4:5)2009"},{"issue":"2","key":"ref30","first-page":"1","article-title":"Detecting data-flow errors in BPMN 2.0","volume":"1","author":"Von Stackelberg","year":"2014","journal-title":"Open J. Inf. Syst."},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2025.3554353"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2011.04.004"},{"key":"ref33","first-page":"112","article-title":"Use runtime verification to improve the quality of medical care practice","volume-title":"Proc. 38th Int. Conf. Softw. Eng. Compan.","author":"Jiang"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/JSYST.2020.2970748"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp036"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3373270"},{"key":"ref37","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"Lee","year":"2016"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.31577\/cai_2022_4_1025"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2019.2949591"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2023.3328895"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2017.2698640"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13094-6_40"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3736177"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2011.08.004"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2023.3321060"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/WETICE.2016.41"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2023.120511"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.3390\/s20195565"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/SMC53654.2022.9945425"},{"key":"ref50","volume-title":"A novel IoT-enabled system for real-time monitoring home appliances using Petri nets","author":"Yang","year":"2023"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1063\/5.0119328"},{"issue":"1","key":"ref52","first-page":"101","article-title":"Modeling and analyzing reliable cyber-physical systems based on aspect orientation","volume":"17","author":"Chen","year":"2014","journal-title":"J. Appl. Sci. Eng."},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.3390\/app15020680"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2024.3372941"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2024.120816"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51831-8_15"}],"container-title":["IEEE Transactions on Systems, Man, and Cybernetics: Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/6221021\/11173422\/11087805.pdf?arnumber=11087805","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T13:35:03Z","timestamp":1759239303000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11087805\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10]]},"references-count":56,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tsmc.2025.3585039","relation":{},"ISSN":["2168-2216","2168-2232"],"issn-type":[{"value":"2168-2216","type":"print"},{"value":"2168-2232","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10]]}}}