{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T16:58:03Z","timestamp":1787504283787,"version":"build-2736575974"},"reference-count":16,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1109\/memcod.2018.8556970","type":"proceedings-article","created":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T19:57:30Z","timestamp":1544126250000},"page":"1-5","source":"Crossref","is-referenced-by-count":20,"title":["Formal Analysis and Verification of DDS in ROS2"],"prefix":"10.1109","author":[{"given":"Yanan","family":"Liu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaojuan","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rui","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jie","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.57"},{"key":"ref11","first-page":"247","article-title":"Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed  Automata","volume":"67","author":"he","year":"2007","journal-title":"Proc IFIP WG 6 1 Int Conf Formal Techn Netw Distrib Syst"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-44829-2_11","article-title":"Model checking publish-subscribe systems","volume":"2648","author":"garlan","year":"2003","journal-title":"Lecture Notes in Computer Science"},{"key":"ref13","first-page":"403","article-title":"A formal verification method: model checking","volume":"33","author":"yang","year":"2006","journal-title":"Journal of Zhejiang University"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1002\/0470011815.b2a09029"},{"key":"ref15","author":"haoli","year":"2014","journal-title":"Data Distibution Service data-centric publish\/subscribe communication"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","article-title":"PRISM: Probabilistic Symbolic Model Checker","volume":"2324","author":"kwiatkowska","year":"2002","journal-title":"The International Conference on Modelling Techniques and Tools for Computer Performance Evaluation"},{"key":"ref4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-1021-7_26","article-title":"Formal Verification in Robotics: Why and How","author":"espiau","year":"1996","journal-title":"Robotics Research"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/HUMANOIDS.2012.6651538"},{"key":"ref6","first-page":"227","article-title":"The Design and Implementation of Middleware-based and VR-based Software Framework for Distributed Industrial Robot Application in Train Maintenance","author":"song","year":"2007","journal-title":"IEEE International Conference on Robotics and Biomimetics"},{"key":"ref5","author":"yandi","year":"2016","journal-title":"Design and Implementation of Communication Middleware for Robot Based on Publish\/Subscribe Technology"},{"key":"ref8","first-page":"619","article-title":"Design and implementation of data distribution service based on dds","volume":"30","author":"yao","year":"2009","journal-title":"Computer Engineering & Design"},{"key":"ref7","article-title":"Research on data distribution service for real-time systems specification","author":"xie","year":"2006","journal-title":"Ship Electronic Engineering"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MILCOM.2004.1494965"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2968478.2968502"},{"key":"ref9","article-title":"Design and implementation of data distribution service based on DDS","author":"chunpu","year":"2008","journal-title":"Fudan University"}],"event":{"name":"2018 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)","location":"Beijing, China","start":{"date-parts":[[2018,10,15]]},"end":{"date-parts":[[2018,10,18]]}},"container-title":["2018 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8536775\/8556861\/08556970.pdf?arnumber=8556970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T23:30:02Z","timestamp":1643239802000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8556970\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/memcod.2018.8556970","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}