{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T02:57:39Z","timestamp":1763348259767,"version":"3.40.5"},"reference-count":26,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["International Journal of Distributed Sensor Networks"],"published-print":{"date-parts":[[2020,5]]},"abstract":"<jats:p> The architecture model of the Internet of thing system is the primary foundation for the design and implementation of the Internet of thing system. This article discusses the method and practice of time automaton modeling and model checking for the architecture of the Internet of thing system from the state and time dimensions. This article introduces the theory and method of modeling using time automata. And then, combined with the actual need of the elderly health cabin Internet of thing system, a dynamic and fault-tolerant time automaton model is established through a relatively complete architecture modeling. The model checking method verifies that the designed Internet of thing system has no deadlock system activity, service correctness, and timeliness correctness. The results of modeling experiments and model validation show that the reference model of time automata Internet of thing architecture established in this article can better reflect the nature of interaction with the physical world, heterogeneity and large-scale, dynamic, and incompleteness of the Internet of thing system. <\/jats:p>","DOI":"10.1177\/1550147720911008","type":"journal-article","created":{"date-parts":[[2020,5,9]],"date-time":"2020-05-09T11:22:04Z","timestamp":1589023324000},"page":"155014772091100","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":5,"title":["Design and model checking of timed automata oriented architecture for Internet of thing"],"prefix":"10.1177","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4456-5981","authenticated-orcid":false,"given":"Guang","family":"Chen","sequence":"first","affiliation":[{"name":"The Xinjiang Technical Institute of Physics and Chemistry, Chinese Academy of Sciences, Urumqi, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"},{"name":"Jiangsu CAS Nor-West star Information Technology Co., Ltd., Wuxi, China"},{"name":"Research and Development Center for IoT of Chinese Academy of Sciences, Wuxi, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tonghai","family":"Jiang","sequence":"additional","affiliation":[{"name":"The Xinjiang Technical Institute of Physics and Chemistry, Chinese Academy of Sciences, Urumqi, China"},{"name":"Xinjiang Laboratory of Minority Speech and Language Information Processing, Chinese Academy of Sciences, Urumqi, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Wang","sequence":"additional","affiliation":[{"name":"The Xinjiang Technical Institute of Physics and Chemistry, Chinese Academy of Sciences, Urumqi, China"},{"name":"Jiangsu CAS Nor-West star Information Technology Co., Ltd., Wuxi, China"},{"name":"Research and Development Center for IoT of Chinese Academy of Sciences, Wuxi, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Tang","sequence":"additional","affiliation":[{"name":"The Xinjiang Technical Institute of Physics and Chemistry, Chinese Academy of Sciences, Urumqi, China"},{"name":"Jiangsu CAS Nor-West star Information Technology Co., Ltd., Wuxi, China"},{"name":"Research and Development Center for IoT of Chinese Academy of Sciences, Wuxi, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenfei","family":"Ji","sequence":"additional","affiliation":[{"name":"The Xinjiang Technical Institute of Physics and Chemistry, Chinese Academy of Sciences, Urumqi, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"},{"name":"Jiangsu CAS Nor-West star Information Technology Co., Ltd., Wuxi, China"},{"name":"Research and Development Center for IoT of Chinese Academy of Sciences, Wuxi, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2020,5,9]]},"reference":[{"issue":"5","key":"bibr1-1550147720911008","first-page":"853","volume":"39","author":"Chen H-M","year":"2016","journal-title":"Chin J Comput"},{"key":"bibr2-1550147720911008","first-page":"27","volume":"45","author":"Dong-Yue L","year":"2018","journal-title":"Comput Sci"},{"key":"bibr3-1550147720911008","first-page":"19","volume":"9","author":"Yang L","year":"2017","journal-title":"Design Techn Posts and Telecommun"},{"key":"bibr4-1550147720911008","doi-asserted-by":"publisher","DOI":"10.1007\/s11071-018-4421-9"},{"issue":"7","key":"bibr5-1550147720911008","first-page":"1448","volume":"41","author":"Mi B-T","year":"2018","journal-title":"Chin J Comput"},{"key":"bibr6-1550147720911008","doi-asserted-by":"publisher","DOI":"10.1109\/52.469759"},{"key":"bibr7-1550147720911008","doi-asserted-by":"publisher","DOI":"10.3724\/SP.J.1016.2013.00168"},{"key":"bibr8-1550147720911008","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2017.2669263"},{"issue":"4","key":"bibr9-1550147720911008","first-page":"1","volume":"30","author":"Shen S-B","year":"2010","journal-title":"J Nanjing Univ Post Telecommun"},{"key":"bibr10-1550147720911008","first-page":"129","volume":"9","author":"Zhou Q-L","year":"2004","journal-title":"Comput Appl"},{"volume-title":"Formal analysis and application of real-time systems based on UPPAAL and UML","year":"2008","author":"Li-Fang Z.","key":"bibr11-1550147720911008"},{"issue":"6","key":"bibr12-1550147720911008","first-page":"1770","volume":"34","author":"Liu M","year":"2014","journal-title":"J Comput Appl"},{"key":"bibr13-1550147720911008","doi-asserted-by":"publisher","DOI":"10.3724\/SP.J.1016.2011.01365"},{"issue":"4","key":"bibr14-1550147720911008","first-page":"730","volume":"26","author":"Han D-S","year":"2015","journal-title":"J Software"},{"key":"bibr15-1550147720911008","first-page":"190","volume":"15","author":"Hua G","year":"2006","journal-title":"Microcomput Inform"},{"key":"bibr16-1550147720911008","first-page":"87","volume-title":"Lectures on concurrency and petri nets","author":"Bengtsson J","year":"2003"},{"volume-title":"Research and implementation of real-time system modeling and formal verification based on UML and UPPAAL","year":"2017","author":"Le X.","key":"bibr17-1550147720911008"},{"issue":"1","key":"bibr18-1550147720911008","first-page":"209","volume":"40","author":"Ting L","year":"2019","journal-title":"Comput Eng Design"},{"issue":"6","key":"bibr19-1550147720911008","first-page":"1699","volume":"29","author":"Meng Y","year":"2018","journal-title":"J Software"},{"issue":"10","key":"bibr20-1550147720911008","first-page":"126","volume":"60","author":"Xiang Z","year":"2016","journal-title":"Railway Stand Design"},{"issue":"9","key":"bibr21-1550147720911008","first-page":"104","volume":"26","author":"Xian-Li J","year":"2016","journal-title":"Comput Techn Develop"},{"volume-title":"Proceedings of international conference on the quantitative evaluation of systems","author":"Behrmann G","key":"bibr22-1550147720911008"},{"first-page":"4","volume-title":"Proceedings of the 8th IEEE international conference on software engineering and service science (ICSESS)","author":"Yan X","key":"bibr23-1550147720911008"},{"key":"bibr24-1550147720911008","doi-asserted-by":"publisher","DOI":"10.1155\/2018\/4071743"},{"volume-title":"Proceedings of international conference on computer aided verification","author":"Henzinger TA","key":"bibr25-1550147720911008"},{"key":"bibr26-1550147720911008","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"}],"container-title":["International Journal of Distributed Sensor Networks"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/1550147720911008","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/1550147720911008","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/1550147720911008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,9]],"date-time":"2020-05-09T11:22:31Z","timestamp":1589023351000},"score":1,"resource":{"primary":{"URL":"http:\/\/journals.sagepub.com\/doi\/10.1177\/1550147720911008"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5]]},"references-count":26,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,5]]}},"alternative-id":["10.1177\/1550147720911008"],"URL":"https:\/\/doi.org\/10.1177\/1550147720911008","relation":{},"ISSN":["1550-1477","1550-1477"],"issn-type":[{"type":"print","value":"1550-1477"},{"type":"electronic","value":"1550-1477"}],"subject":[],"published":{"date-parts":[[2020,5]]}}}