{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:26:21Z","timestamp":1725902781565},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319592879"},{"type":"electronic","value":"9783319592886"}],"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:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-59288-6_61","type":"book-chapter","created":{"date-parts":[[2017,7,4]],"date-time":"2017-07-04T06:42:50Z","timestamp":1499150570000},"page":"609-614","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modelling and Analysis of TCP for Nodes Communication with ROS"],"prefix":"10.1007","author":[{"given":"Xiaojuan","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanyan","family":"Huo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rui","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,5]]},"reference":[{"key":"61_CR1","unstructured":"Huang, Z.: The real-time operating system development and implemen- tation for industrial robot controller. School of Mechanical Engineering & Automation, Beijing University of Aeronautics, Beijing (2013)"},{"issue":"10","key":"61_CR2","first-page":"2657","volume":"31","author":"H Han","year":"2011","unstructured":"Han, H.: Improvement for wireless TCP based on bit error rate monitoring. J. Comput. Appl. 31(10), 2657\u20132659 (2011)","journal-title":"J. Comput. Appl."},{"issue":"1","key":"61_CR3","first-page":"103","volume":"42","author":"M Li","year":"2016","unstructured":"Li, M., Zhang, Y., Xiang, D.: Improvement mechanism of transmission control protocol in wireless network. Comput. Eng. 42(1), 103\u2013108 (2016)","journal-title":"Comput. Eng."},{"issue":"1","key":"61_CR4","first-page":"124","volume":"37","author":"S Wei","year":"2016","unstructured":"Wei, S., Yang, W., Shen, Y.: A secret communication method based on reliable packet ordering. J. Chin. Comput. Syst. 37(1), 124\u2013128 (2016)","journal-title":"J. Chin. Comput. Syst."},{"issue":"6A","key":"61_CR5","first-page":"1","volume":"40","author":"Z Wang","year":"2013","unstructured":"Wang, Z.: Survey of model checking. Comput. Sci. 40(6A), 1\u201314 (2013)","journal-title":"Comput. Sci."},{"key":"61_CR6","unstructured":"PRISM-probabilistic symbolic model checker [EB\/OL] (2011). \nhttp:\/\/www.prismmodelchecker.org\/"},{"issue":"6","key":"61_CR7","first-page":"49","volume":"309","author":"F Li","year":"2009","unstructured":"Li, F.: Formal description and verification of TCP protocol based on colored Petri nets. Mod. Comput. 309(6), 49\u201352 (2009)","journal-title":"Mod. Comput."},{"issue":"9","key":"61_CR8","first-page":"25","volume":"34","author":"Y Li","year":"2013","unstructured":"Li, Y., Li, X., Guan, Y.: Formal modeling and probabilistic analysis of SpaceWire protocol. J. Chin. Comput. Syst. 34(9), 25\u201329 (2013)","journal-title":"J. Chin. Comput. Syst."},{"issue":"10","key":"61_CR9","first-page":"2379","volume":"36","author":"Y Wang","year":"2015","unstructured":"Wang, Y., Wang, R., Guan, Y.: Formal verification of node to node communication in RGMP-ROS hybrid operating system. J. Chin. Comput. Syst. 36(10), 2379\u20132383 (2015)","journal-title":"J. Chin. Comput. Syst."},{"key":"61_CR10","unstructured":"Parker, D.A.: Implementation of Symbolic Model Checking for Probabilistic Systems. University of Birmingham (2002)"},{"issue":"11","key":"61_CR11","first-page":"1798","volume":"28","author":"K Su","year":"2005","unstructured":"Su, K., Luo, X., Lu, G.: Symbolic model checking for CTL. Chin. J. Comput. 28(11), 1798\u20131806 (2005)","journal-title":"Chin. J. Comput."},{"key":"61_CR12","unstructured":"TCP three-way-handshake and four recovery summary [EB\/OL]. \nhttp:\/\/blog.csdn.net"},{"key":"61_CR13","unstructured":"Li, Z.: Research on design of intelligent gateway in substation. Jiangsu university of science and technology (2007)"},{"key":"61_CR14","unstructured":"Liu, Y.: Research on reliability design and test method of device driver. University of Electronic Science and technology (2014)"},{"key":"61_CR15","unstructured":"Wu, Y.: Design of P2P instant messaging software based on XMPP protocol. Electronic information technology and instruments of Zhejiang University, Hangzhou (2007)"}],"container-title":["Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","Collaborate Computing: Networking, Applications and Worksharing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-59288-6_61","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,4]],"date-time":"2017-07-04T07:05:11Z","timestamp":1499151911000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-59288-6_61"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319592879","9783319592886"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-59288-6_61","relation":{},"ISSN":["1867-8211","1867-822X"],"issn-type":[{"type":"print","value":"1867-8211"},{"type":"electronic","value":"1867-822X"}],"subject":[],"published":{"date-parts":[[2017]]}}}