TY - GEN
T1 - Modeling and Verifying HDFS Using CSP
AU - Xie, Wanling
AU - Zhu, Huibiao
AU - Wu, Xi
AU - Xiang, Shuangqing
AU - Guo, Jian
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/8/24
Y1 - 2016/8/24
N2 - Hadoop Distributed File System (HDFS) is a high fault-tolerant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Since HDFS is widely used, analysis on it in a formal framework is of great significance. In this paper, we use Communicating Sequential Processes (CSP) to model and analyze HDFS. We mainly focus on the dominant parts which include reading files and writing files in HDFS and formalize them in detail. Moreover, we use the model checker Process Analysis Toolkit (PAT) to simulate the model constructed and verify whether it caters for the specification and some important properties, including Deadlock-freeness, Minimal Distance Scheme, Mutual Exclusion, Write-Once Scheme and Robustness.
AB - Hadoop Distributed File System (HDFS) is a high fault-tolerant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Since HDFS is widely used, analysis on it in a formal framework is of great significance. In this paper, we use Communicating Sequential Processes (CSP) to model and analyze HDFS. We mainly focus on the dominant parts which include reading files and writing files in HDFS and formalize them in detail. Moreover, we use the model checker Process Analysis Toolkit (PAT) to simulate the model constructed and verify whether it caters for the specification and some important properties, including Deadlock-freeness, Minimal Distance Scheme, Mutual Exclusion, Write-Once Scheme and Robustness.
UR - https://www.scopus.com/pages/publications/84988027253
U2 - 10.1109/COMPSAC.2016.158
DO - 10.1109/COMPSAC.2016.158
M3 - 会议稿件
AN - SCOPUS:84988027253
T3 - Proceedings - International Computer Software and Applications Conference
SP - 221
EP - 226
BT - Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016
A2 - Claycomb, William
A2 - Milojicic, Dejan
A2 - Liu, Ling
A2 - Matskin, Mihhail
A2 - Zhang, Zhiyong
A2 - Reisman, Sorel
A2 - Sato, Hiroyuki
A2 - Zhang, Zhiyong
A2 - Ahamed, Sheikh Iqbal
PB - IEEE Computer Society
T2 - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016
Y2 - 10 June 2016 through 14 June 2016
ER -