{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T16:30:58Z","timestamp":1748968258130},"reference-count":15,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"12","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2021,12,1]]},"DOI":"10.1587\/transinf.2021edp7070","type":"journal-article","created":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T22:41:41Z","timestamp":1638312101000},"page":"2154-2163","source":"Crossref","is-referenced-by-count":3,"title":["Formalization and Analysis of Ceph Using Process Algebra"],"prefix":"10.1587","volume":"E104.D","author":[{"given":"Ran","family":"LI","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"ZHU","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiaqi","family":"YIN","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] B. Li, M. Wang, Y. Zhao, G. Pu, H. Zhu, and F. Song, \u201cModeling and verifying google file system,\u201d 2015 IEEE 16th International Symposium on High Assurance Systems Engineering, pp.207-214, IEEE, 2015. 10.1109\/hase.2015.38","DOI":"10.1109\/HASE.2015.38"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] W. Xie, H. Zhu, X. Wu, S. Xiang, J. Guo, and P.C. Vinh, \u201cModeling and verifying hdfs using process algebra,\u201d Mobile Networks and Applications, vol.22, no.2, pp.318-331, 2017. 10.1007\/s11036-017-0812-2","DOI":"10.1007\/s11036-017-0812-2"},{"key":"3","unstructured":"[3] S.A. Weil, \u201cCeph: reliable, scalable, and high-performance distributed storage,\u201d Ph.D. thesis, University of California, Santa Cruz, 2007."},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] X. Shi, Y. Ji, H. Xie, and Y. Lu, \u201cA prefetching mechanism based on moosefs,\u201d International Conference on Trustworthy Computing and Services, pp.146-153, Springer, 2013. 10.1007\/978-3-662-43908-1_19","DOI":"10.1007\/978-3-662-43908-1_19"},{"key":"5","unstructured":"[5] S.A. Weil, S.A. Brandt, E.L. Miller, D.D. Long, and C. Maltzahn, \u201cCeph: A scalable, high-performance distributed file system,\u201d Proc. 7th Symposium on Operating systems design and implementation, pp.307-320, 2006."},{"key":"6","unstructured":"[6] Ceph, \u201cCeph storage,\u201d https:\/\/ceph.io\/ceph-storage\/, accessed March 31. 2021."},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] C.T. Yang, E. Kristiani, Y.T. Wang, G. Min, C.H. Lai, and W.J. Jiang, \u201cOn construction of a network log management system using elk stack with ceph,\u201d The Journal of Supercomputing, pp.1-17, 2019.","DOI":"10.1007\/s11227-019-02853-2"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] D. Gudu, M. Hardt, and A. Streit, \u201cEvaluating the performance and scalability of the ceph distributed storage system,\u201d IEEE International Conference on Big Data, Washington, DC, USA, Oct. 27-30, 2014, pp.177-182, 2014. 10.1109\/bigdata.2014.7004229","DOI":"10.1109\/BigData.2014.7004229"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] S. Xiang, H. Zhu, X. Wu, L. Xiao, M. Bonsangue, W. Xie, and L. Zhang, \u201cModeling and verifying the topology discovery mechanism of openflow controllers in software-defined networks using process algebra,\u201d Science of Computer Programming, vol.187, p.102343, 2020. 10.1016\/j.scico.2019.102343","DOI":"10.1016\/j.scico.2019.102343"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] A. Liu, H. Zhu, M. Popovic, S. Xiang, and L. Zhang, \u201cFormal analysis and verification of the pstm architecture using csp,\u201d Journal of Systems and Software, vol.165, p.110559, 2020. 10.1016\/j.jss.2020.110559","DOI":"10.1016\/j.jss.2020.110559"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] G. Lowe and B. Roscoe, \u201cUsing csp to detect errors in the tmn protocol,\u201d IEEE Trans. Softw. Eng., vol.23, no.10, pp.659-669, 1997. 10.1109\/32.637148","DOI":"10.1109\/32.637148"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] A.W. Leung and E.L. Miller, \u201cScalable security for large, high performance storage systems,\u201d Proc. second ACM workshop on Storage security and survivability, pp.29-40, 2006. 10.1145\/1179559.1179565","DOI":"10.1145\/1179559.1179565"},{"key":"13","unstructured":"[13] C. Maltzahn, E. Molina-Estolano, A. Khurana, A.J. Nelson, S.A. Brandt, and S. Weil, \u201cCeph as a scalable alternative to the hadoop distributed file system,\u201d login: The USENIX Magazine, vol.35, pp.38-49, 2010."},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] J. Kohl, C. Neuman, et al., \u201cThe kerberos network authentication service (v5),\u201d Tech. Rep., RFC 1510, Sept. 1993.","DOI":"10.17487\/rfc1510"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] C.A.R. Hoare, \u201cCommunicating sequential processes,\u201d Communications of the ACM, vol.21, no.8, pp.666-677, 1978. 10.1145\/359576.359585","DOI":"10.1145\/359576.359585"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/12\/E104.D_2021EDP7070\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,4]],"date-time":"2021-12-04T03:47:50Z","timestamp":1638589670000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/12\/E104.D_2021EDP7070\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,1]]},"references-count":15,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2021]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2021edp7070","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,1]]},"article-number":"2021EDP7070"}}