{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T21:54:09Z","timestamp":1740174849640,"version":"3.37.3"},"reference-count":22,"publisher":"Wiley","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61133007"],"award-info":[{"award-number":["61133007"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mobile Information Systems"],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:p>Mobile cyber-physical systems (CPSs) are very hard to verify, because of asynchronous communication and the arbitrary number of components. Verification via model checking typically becomes impracticable due to the state space explosion caused by the system parameters and concurrency. In this paper, we propose a formal approach to verify the safety properties of parameterized protocols in mobile CPS. By using counter abstraction, the protocol is modeled as a Petri net. Then, a novel algorithm, which uses IC3 (the state-of-the-art model checking algorithm) as the back-end engine, is presented to verify the Petri net model. The experimental results show that our new approach can greatly scale the verification capabilities compared favorably against several recently published approaches. In addition to solving the instances fast, our method is significant for its lower memory consumption.<\/jats:p>","DOI":"10.1155\/2017\/5731678","type":"journal-article","created":{"date-parts":[[2017,5,11]],"date-time":"2017-05-11T08:29:45Z","timestamp":1494491385000},"page":"1-10","source":"Crossref","is-referenced-by-count":7,"title":["A Formal Approach to Verify Parameterized Protocols in Mobile Cyber-Physical Systems"],"prefix":"10.1155","volume":"2017","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1633-4051","authenticated-orcid":true,"given":"Long","family":"Zhang","sequence":"first","affiliation":[{"name":"College of Computer, National University of Defense Technology, Changsha, China"}]},{"given":"Wenyan","family":"Hu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}]},{"given":"Wanxia","family":"Qu","sequence":"additional","affiliation":[{"name":"College of Computer, National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9050-0866","authenticated-orcid":true,"given":"Yang","family":"Guo","sequence":"additional","affiliation":[{"name":"College of Computer, National University of Defense Technology, Changsha, China"}]},{"given":"Sikun","family":"Li","sequence":"additional","affiliation":[{"name":"College of Computer, National University of Defense Technology, Changsha, China"}]}],"member":"311","reference":[{"key":"2","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2011.10.001"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/s13174-010-0004-9"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2015.2435746"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2014.2371813"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2015.2395959"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"issue":"1","key":"9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2200\/S00658ED1V01Y201508DCT013","volume":"6","year":"2015","journal-title":"Synthesis Lectures on Distributed Computing Theory"},{"year":"1999","key":"12"},{"key":"13","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-1-4615-3190-6_3","volume-title":"Symbolic model checking","year":"1993"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2011.2160000"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.09.011"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/tetc.2013.2273359"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2014.6829948"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90026-6"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1145\/2842603"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/11916246_16"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/s11227-012-0755-0"},{"issue":"6","key":"33","first-page":"991","volume":"26","year":"2014","journal-title":"Journal of Computer-Aided Design and Computer Graphics"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"issue":"53","key":"39","volume":"2005","year":"2005","journal-title":"SAT"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.001"}],"container-title":["Mobile Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/misy\/2017\/5731678.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/misy\/2017\/5731678.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/misy\/2017\/5731678.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,5,11]],"date-time":"2017-05-11T08:29:55Z","timestamp":1494491395000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/misy\/2017\/5731678\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":22,"alternative-id":["5731678","5731678"],"URL":"https:\/\/doi.org\/10.1155\/2017\/5731678","relation":{},"ISSN":["1574-017X","1875-905X"],"issn-type":[{"type":"print","value":"1574-017X"},{"type":"electronic","value":"1875-905X"}],"subject":[],"published":{"date-parts":[[2017]]}}}