{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:51:29Z","timestamp":1761490289534,"version":"3.37.3"},"reference-count":20,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Science Foundation of China","doi-asserted-by":"publisher","award":["61100066"],"award-info":[{"award-number":["61100066"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2017]]},"DOI":"10.1109\/access.2017.2708127","type":"journal-article","created":{"date-parts":[[2017,5,26]],"date-time":"2017-05-26T18:16:53Z","timestamp":1495822613000},"page":"10882-10891","source":"Crossref","is-referenced-by-count":11,"title":["A Multi-Perspective Method for Analysis of Cooperative Behaviors Among Industrial Devices of Smart Factory"],"prefix":"10.1109","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6683-2884","authenticated-orcid":false,"given":"Gang","family":"Ren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qingsong","family":"Hua","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pan","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwei","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2015.07.015"},{"key":"ref11","first-page":"317","article-title":"A formal approach for modeling and verification of distributed systems","author":"ren","year":"2015","journal-title":"Proc Cloud"},{"key":"ref12","first-page":"1","article-title":"Formal semantics of UML sequence diagram for safety-critical systems","volume":"11","author":"ren","year":"2015","journal-title":"J Comput Inf Syst"},{"journal-title":"OMG Unified Modeling Language (OMG UML) Report OMG","year":"2015","key":"ref13"},{"key":"ref14","first-page":"479","article-title":"An introduction to the $\\pi $ -calculus","volume":"179","author":"parrow","year":"2000","journal-title":"Bergstra Ponse Smolka Handbook Process Algebra"},{"article-title":"A brief introduction to mobility workbench (MWB)","year":"2005","author":"bundgaard","key":"ref15"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An opensource tool for symbolic model checking","volume":"2404","author":"cimatti","year":"2002","journal-title":"Computer Aided Verification"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2004.1316717"},{"article-title":"Symbolic model checking: An approach to the state explosion problem","year":"1992","author":"mcmillan","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/66.705370"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/MWC.2016.7721738"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2015.12.017"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2015.2437951"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1109\/ICSE.2002.1007998","article-title":"Safety Critical Systems: Challenges and Directions","author":"john c knight","year":"2002","journal-title":"Proceedings of the 24th International Conference on Software Engineering ICSE 2002"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2016.2519381"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2015.2416657"},{"key":"ref2","article-title":"A manufacturing big data solution for active preventive maintenance","author":"wan","year":"0","journal-title":"IEEE Trans Ind Informat"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/JSEN.2016.2565621"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s11235-011-9643-9"},{"journal-title":"Model checking","year":"2000","author":"clarke","key":"ref20"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/7859429\/07934301.pdf?arnumber=7934301","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:29:56Z","timestamp":1642004996000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7934301\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/access.2017.2708127","relation":{},"ISSN":["2169-3536"],"issn-type":[{"type":"electronic","value":"2169-3536"}],"subject":[],"published":{"date-parts":[[2017]]}}}