Modeling and Verifying HDFS Using CSP

Wanling Xie; Huibiao Zhu; Xi Wu; Shuangqing Xiang; Jian Guo

doi:10.1109/COMPSAC.2016.158

Modeling and Verifying HDFS Using CSP

Wanling Xie, Huibiao Zhu, Xi Wu, Shuangqing Xiang, Jian Guo

Software Engineering Institute

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 Scopus citations

Abstract

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.

Original language	English
Title of host publication	Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016
Editors	William Claycomb, Dejan Milojicic, Ling Liu, Mihhail Matskin, Zhiyong Zhang, Sorel Reisman, Hiroyuki Sato, Zhiyong Zhang, Sheikh Iqbal Ahamed
Publisher	IEEE Computer Society
Pages	221-226
Number of pages	6
ISBN (Electronic)	9781467388450
DOIs	https://doi.org/10.1109/COMPSAC.2016.158
State	Published - 24 Aug 2016
Event	2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016 - Atlanta, United States Duration: 10 Jun 2016 → 14 Jun 2016

Publication series

Name	Proceedings - International Computer Software and Applications Conference
Volume	1
ISSN (Print)	0730-3157

Conference

Conference	2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016
Country/Territory	United States
City	Atlanta
Period	10/06/16 → 14/06/16

Access to Document

10.1109/COMPSAC.2016.158

Cite this

Xie, W., Zhu, H., Wu, X., Xiang, S., & Guo, J. (2016). Modeling and Verifying HDFS Using CSP. In W. Claycomb, D. Milojicic, L. Liu, M. Matskin, Z. Zhang, S. Reisman, H. Sato, Z. Zhang, & S. I. Ahamed (Eds.), Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016 (pp. 221-226). Article 7552012 (Proceedings - International Computer Software and Applications Conference; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/COMPSAC.2016.158

Xie, Wanling ; Zhu, Huibiao ; Wu, Xi et al. / Modeling and Verifying HDFS Using CSP. Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016. editor / William Claycomb ; Dejan Milojicic ; Ling Liu ; Mihhail Matskin ; Zhiyong Zhang ; Sorel Reisman ; Hiroyuki Sato ; Zhiyong Zhang ; Sheikh Iqbal Ahamed. IEEE Computer Society, 2016. pp. 221-226 (Proceedings - International Computer Software and Applications Conference).

@inproceedings{ed2242325ae64c77b7fa6c4eb0674713,

title = "Modeling and Verifying HDFS Using CSP",

abstract = "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.",

author = "Wanling Xie and Huibiao Zhu and Xi Wu and Shuangqing Xiang and Jian Guo",

note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016 ; Conference date: 10-06-2016 Through 14-06-2016",

year = "2016",

month = aug,

day = "24",

doi = "10.1109/COMPSAC.2016.158",

language = "英语",

series = "Proceedings - International Computer Software and Applications Conference",

publisher = "IEEE Computer Society",

pages = "221--226",

editor = "William Claycomb and Dejan Milojicic and Ling Liu and Mihhail Matskin and Zhiyong Zhang and Sorel Reisman and Hiroyuki Sato and Zhiyong Zhang and Ahamed, \{Sheikh Iqbal\}",

booktitle = "Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016",

address = "美国",

}

Xie, W, Zhu, H, Wu, X, Xiang, S & Guo, J 2016, Modeling and Verifying HDFS Using CSP. in W Claycomb, D Milojicic, L Liu, M Matskin, Z Zhang, S Reisman, H Sato, Z Zhang & SI Ahamed (eds), Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016., 7552012, Proceedings - International Computer Software and Applications Conference, vol. 1, IEEE Computer Society, pp. 221-226, 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016, Atlanta, United States, 10/06/16. https://doi.org/10.1109/COMPSAC.2016.158

Modeling and Verifying HDFS Using CSP. / Xie, Wanling; Zhu, Huibiao; Wu, Xi et al.
Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016. ed. / William Claycomb; Dejan Milojicic; Ling Liu; Mihhail Matskin; Zhiyong Zhang; Sorel Reisman; Hiroyuki Sato; Zhiyong Zhang; Sheikh Iqbal Ahamed. IEEE Computer Society, 2016. p. 221-226 7552012 (Proceedings - International Computer Software and Applications Conference; Vol. 1).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Modeling and Verifying HDFS Using CSP

AU - Xie, Wanling

AU - Zhu, Huibiao

AU - Wu, Xi

AU - Xiang, Shuangqing

AU - Guo, Jian

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 -

Xie W, Zhu H, Wu X, Xiang S, Guo J. Modeling and Verifying HDFS Using CSP. In Claycomb W, Milojicic D, Liu L, Matskin M, Zhang Z, Reisman S, Sato H, Zhang Z, Ahamed SI, editors, Proceedings - 2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016. IEEE Computer Society. 2016. p. 221-226. 7552012. (Proceedings - International Computer Software and Applications Conference). doi: 10.1109/COMPSAC.2016.158

Modeling and Verifying HDFS Using CSP

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this