{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:43:07Z","timestamp":1777596187840,"version":"3.51.4"},"reference-count":51,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"2","license":[{"start":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T00:00:00Z","timestamp":1527811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61420106004"],"award-info":[{"award-number":["61420106004"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61732013"],"award-info":[{"award-number":["61732013"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61751207"],"award-info":[{"award-number":["61751207"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61572386"],"award-info":[{"award-number":["61572386"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Rel."],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1109\/tr.2018.2806349","type":"journal-article","created":{"date-parts":[[2018,3,19]],"date-time":"2018-03-19T22:10:09Z","timestamp":1521497409000},"page":"481-493","source":"Crossref","is-referenced-by-count":18,"title":["A Novel Approach to Modeling and Verifying Real-Time Systems for High Reliability"],"prefix":"10.1109","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2772-1433","authenticated-orcid":false,"given":"Jin","family":"Cui","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3119-3242","authenticated-orcid":false,"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-4580","authenticated-orcid":false,"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]},{"given":"Hongwei","family":"Du","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","year":"0"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.039"},{"key":"ref33","doi-asserted-by":"crossref","first-page":"762","DOI":"10.1007\/s11704-016-6059-4","article-title":"MSVL: A typed language for temporal logic\n programming","volume":"11","author":"wang","year":"2017","journal-title":"Frontiers Comput Sci"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-015-0882-6"},{"key":"ref31","first-page":"167","article-title":"A unified model checking approach with projection temporal logic","author":"duan","year":"0","journal-title":"Formal Methods and Software Engineering"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.001"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.02.011"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.98"},{"key":"ref35","author":"labrosse","year":"2009","journal-title":"uC\/OS-II - the real-time kernel"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.02.037"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BF02944904"},{"key":"ref27","author":"duan","year":"2005","journal-title":"Temporal Logic and Temporal Logic Programming"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"key":"ref2","article-title":"Smart house management and control without customer inconvenience","author":"alquthami","year":"0","journal-title":"IEEE Trans Smart Grid"},{"key":"ref1","first-page":"414","article-title":"Model-checking for real-time systems","author":"alur","year":"0","journal-title":"Proc IEEE 5th Symp Logic in Computer Science"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1083"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","article-title":"State\/event-based software model checking","volume":"41","author":"chaki","year":"2004","journal-title":"5th International Conference on Integrated Formal Methods"},{"key":"ref26","article-title":"An extended interval temporal logic and a framing technique for\n temporal logic programming","author":"duan","year":"1996"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"ref50","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/2984450.2984459","article-title":"Unmanned aircraft systems in the\n national airspace system: A formal methods perspective","volume":"3","author":"munoz","year":"2016","journal-title":"ACM SIGLOG News"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2406860"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2456853"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2016.2618121"},{"key":"ref40","first-page":"329","article-title":"Extending Promela and Spin for real time","author":"tripakis","year":"1996","journal-title":"International Workshop on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref12","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref13","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.2050199"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1002\/dac.3447"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430537"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-007-9036-z"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.04.042"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2964202"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2015.2472367"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2015.2470247"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2007.05.036"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.3357\/ASEM.3292.2013"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/52.819971"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2006.12.540"},{"key":"ref49","first-page":"116","article-title":"Formal\n specification and synthesis of mission plans for unmanned aerial vehicles","author":"humphrey","year":"0","journal-title":"Proc AAAI Spring Symp"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2508559"},{"key":"ref46","first-page":"209","article-title":"KLEE:\n Unassisted and automatic generation of high-coverage tests for complex systems programs","volume":"8","author":"cadar","year":"0","journal-title":"Proc Operating Syst Des Implementation"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.10.004"},{"key":"ref48","doi-asserted-by":"crossref","first-page":"1105","DOI":"10.2298\/CSIS120326018W","article-title":"From machine-to-machine communications towards cyber-physical systems","volume":"10","author":"wan","year":"2013","journal-title":"Comput Sci Inf Syst"},{"key":"ref47","first-page":"358","article-title":"Formal verification of cyber-physical systems: Coping with continuous elements","author":"sanwal","year":"2013","journal-title":"International Conference on Computational Science and its Applications"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_48"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055357"},{"key":"ref44","first-page":"709","article-title":"PAT: Towards flexible verification under fairness","author":"sun","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2011.11"}],"container-title":["IEEE Transactions on Reliability"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/24\/8370165\/08319514.pdf?arnumber=8319514","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T05:49:52Z","timestamp":1643176192000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8319514\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6]]},"references-count":51,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.1109\/tr.2018.2806349","relation":{},"ISSN":["0018-9529","1558-1721"],"issn-type":[{"value":"0018-9529","type":"print"},{"value":"1558-1721","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6]]}}}