{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T16:29:56Z","timestamp":1748968196637},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T00:00:00Z","timestamp":1487203200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s11036-017-0812-2","type":"journal-article","created":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T07:16:10Z","timestamp":1487229370000},"page":"318-331","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Modeling and Verifying HDFS Using Process Algebra"],"prefix":"10.1007","volume":"22","author":[{"given":"Wanling","family":"Xie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xi","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuangqing","family":"Xiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"key":"812_CR1","doi-asserted-by":"publisher","unstructured":"Azzedin F (2013) Towards a scalable HDFS architecture 2013 International conference on collaboration technologies and systems, CTS 2013, San Diego, CA, USA, May 20-24, 2013, pp 155\u2013161. doi: 10.1109\/CTS.2013.6567222","DOI":"10.1109\/CTS.2013.6567222"},{"key":"812_CR2","doi-asserted-by":"publisher","unstructured":"Bergstra JA, Klop JW (1985) Algebra of communicating processes with abstraction. Theor Comput Sci 37:77-121. doi: 10.1016\/0304-3975(85)90088-X .","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"812_CR3","doi-asserted-by":"publisher","unstructured":"Bui D, Hussain S, Huh E, Lee S (2016) Adaptive replication management in HDFS based on supervised learning. IEEE Trans Knowl Data Eng 28(6):1369-1382. doi: 10.1109\/TKDE.2016.2523510 .","DOI":"10.1109\/TKDE.2016.2523510"},{"key":"812_CR4","doi-asserted-by":"publisher","unstructured":"Buyya R, Yeo CS, Venugopal S, Broberg J, Brandic I (2009) Cloud computing and emerging IT platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Comp Syst 25(6):599\u2013616. doi: 10.1016\/j.future.2008.12.001 .","DOI":"10.1016\/j.future.2008.12.001"},{"key":"812_CR5","doi-asserted-by":"publisher","unstructured":"Dean J, Ghemawat S (2008) Mapreduce: simplified data processing on large clusters. Commun ACM 51(1):107\u2013113. doi: 10.1145\/1327452.1327492 .","DOI":"10.1145\/1327452.1327492"},{"key":"812_CR6","doi-asserted-by":"publisher","unstructured":"Dong B, Zheng Q, Tian F, Chao K, Ma R, Anane R (2012) An optimized approach for storing and accessing small files on cloud storage. J Network and Computer Applications 35(6):1847-1862. doi: 10.1016\/j.jnca.2012.07.009 .","DOI":"10.1016\/j.jnca.2012.07.009"},{"key":"812_CR7","doi-asserted-by":"publisher","unstructured":"Dong B, Zheng Q, Tian F, Chao K, Godwin N, Ma T, Xu H (2014) Performance models and dynamic characteristics analysis for HDFS write and read operations: A systematic view. J Syst Softw 93:132\u2013151. doi: 10.1016\/j.jss.2014.02.038 .","DOI":"10.1016\/j.jss.2014.02.038"},{"key":"812_CR8","doi-asserted-by":"publisher","unstructured":"Ghemawat S, Gobioff H, Leung S (2003) The google file system Proceedings of the 19th ACM symposium on operating systems principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, pp 29\u201343. doi: 10.1145\/945445.945450","DOI":"10.1145\/945445.945450"},{"key":"812_CR9","unstructured":"Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall International in Computer Science"},{"key":"812_CR10","doi-asserted-by":"publisher","unstructured":"Liu Y, Sun J, Dong JS (2010) Analyzing hierarchical complex real-time systems. In: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 7-11, 2010, pp 365-366. doi: 10.1145\/1882291.1882350","DOI":"10.1145\/1882291.1882350"},{"key":"812_CR11","doi-asserted-by":"publisher","unstructured":"Lowe G, Davies J (1999) Using CSP to verify sequential consistency. Distributed Computing 12(2-3):91-103. doi: 10.1007\/s004460050060 .","DOI":"10.1007\/s004460050060"},{"key":"812_CR12","doi-asserted-by":"publisher","unstructured":"Lowe G, Roscoe AW (1997) Using CSP, to detect errors in the TMN protocol. IEEE Trans Software Eng 23(10):659\u2013669. doi: 10.1109\/32.637148 .","DOI":"10.1109\/32.637148"},{"key":"812_CR13","doi-asserted-by":"publisher","unstructured":"Mazur T, Lowe G (2014) Csp-based counter abstraction for systems with node identifiers. Sci Comput Program 81:3\u201352. doi: 10.1016\/j.scico.2013.03.018 .","DOI":"10.1016\/j.scico.2013.03.018"},{"key":"812_CR14","doi-asserted-by":"crossref","unstructured":"Milner R (1980) A Calculus of Communicating Systems, vol 92, Springer. Lecture Notes in Computer Science","DOI":"10.1007\/3-540-10235-3"},{"key":"812_CR15","unstructured":"Roscoe AW (1997) The Theory and Practice of Concurrency. Prentice Hall International in Computer Science"},{"key":"812_CR16","unstructured":"Roscoe AW (2007) Understanding Concurrent Systems, Springer Verlag"},{"key":"812_CR17","doi-asserted-by":"publisher","unstructured":"Roscoe AW, Huang J (2013) Checking noninterference in timed CSP. Formal Asp Comput 25(1):3-35. doi: 10.1007\/s00165-012-0251-6 .","DOI":"10.1007\/s00165-012-0251-6"},{"key":"812_CR18","doi-asserted-by":"publisher","unstructured":"Shafer J, Rixner S, Cox AL (2010) The hadoop distributed filesystem: Balancing portability and performance. In: IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2010, www.ispass.org, 28-30 March 2010, White Plains, NY, USA, pp 122\u2013133. doi: 10.1109\/ISPASS.2010.5452045","DOI":"10.1109\/ISPASS.2010.5452045"},{"key":"812_CR19","doi-asserted-by":"crossref","unstructured":"Shvachko K, Kuang H, Radia S, Chansler R (2010) The hadoop distributed file system. In: IEEE 26th symposium on mass storage systems and technologies, MSST 2012, Lake Tahoe, Nevada, USA, May 3-7, 2010, pp 1\u201310","DOI":"10.1109\/MSST.2010.5496972"},{"key":"812_CR20","doi-asserted-by":"publisher","unstructured":"Si Y, Sun J, Liu Y, Dong JS, Pang J, Zhang SJ, Yang X (2014) Model checking with fairness assumptions using PAT. Frontiers of Computer Science 8(1):1\u201316. doi: 10.1007\/s11704-013-3091-5 .","DOI":"10.1007\/s11704-013-3091-5"},{"key":"812_CR21","doi-asserted-by":"publisher","unstructured":"Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: Introducing a process analysis toolkit. In: Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 3rd International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008, pp 307\u2013322. doi: 10.1007\/978-3-540-88479-8_22","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"812_CR22","doi-asserted-by":"publisher","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) Pat: Towards flexible verification under fairness. In: Proceedings of the 21th international conference on computer aided verification (CAV\u201909), Springer, lecture notes in computer science, vol 5643, pp 709\u2013714. doi: 10.1007\/978-3-642-02658-4_59","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"812_CR23","doi-asserted-by":"publisher","unstructured":"Sun J, Liu Y, Song S, Dong JS, Li X (2011) PRTS: An approach for model checking probabilistic real-time hierarchical systems. In: Proceedings of the Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011, pp 147-162. doi: 10.1007\/978-3-642-24559-6_12","DOI":"10.1007\/978-3-642-24559-6_12"},{"key":"812_CR24","doi-asserted-by":"publisher","unstructured":"Sun J, Liu Y, Dong J S, Liu Y, Shi L, Andr\u00e9 \u00c9 (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3. doi: 10.1145\/2430536.2430537 .","DOI":"10.1145\/2430536.2430537"},{"key":"812_CR25","doi-asserted-by":"publisher","unstructured":"Tian F, Ma T, Dong B, Zheng Q (2015) Pwlm3-based automatic performance model estimation method for HDFS write and read operations. Future Generation Comp Syst 50:127-139. doi: 10.1016\/j.future.2015.01.011 .","DOI":"10.1016\/j.future.2015.01.011"},{"key":"812_CR26","doi-asserted-by":"publisher","unstructured":"Wang F, Qiu J, Yang J, Dong B, Li X H, Li Y (2009) Hadoop high availability through metadata replication Proceedings of the First International CIKM Workshop on Cloud Data Management, CloudDb 2009, Hong Kong, China, November 2, 2009, pp 37-44. doi: 10.1145\/1651263.1651271","DOI":"10.1145\/1651263.1651271"},{"key":"812_CR27","doi-asserted-by":"publisher","unstructured":"Wu X, Zhu H, Zhao Y, Wang Z, Liu S (2013) Modeling and verifying the ariadne protocol using process algebra. Comput Sci Inf Syst 10(1):393-421. doi: 10.2298\/CSIS120601009W .","DOI":"10.2298\/CSIS120601009W"},{"key":"812_CR28","doi-asserted-by":"publisher","unstructured":"Zhang Q, Cheng L, Boutaba R (2010) Cloud computing: state-of-the-art and research challenges. J Internet Services and Applications 1(1):7-18. doi: 10.1007\/s13174-010-0007-6 .","DOI":"10.1007\/s13174-010-0007-6"},{"key":"812_CR29","doi-asserted-by":"publisher","unstructured":"Zhu Y, Hu H, Ahn G, Yau SS (2012) Efficient audit service outsourcing for data integrity in clouds. J Syst Softw 85(5):1083\u20131095. doi: 10.1016\/j.jss.2011.12.024 .","DOI":"10.1016\/j.jss.2011.12.024"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-017-0812-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11036-017-0812-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-017-0812-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T06:41:59Z","timestamp":1498372919000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11036-017-0812-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,16]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["812"],"URL":"https:\/\/doi.org\/10.1007\/s11036-017-0812-2","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"value":"1383-469X","type":"print"},{"value":"1572-8153","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,16]]}}}