Formalizing google file system

Mengdi Wang; Bo Li; Yongxin Zhao; Geguang Pu

doi:10.1109/PRDC.2014.32

Formalizing google file system

Mengdi Wang
, Bo Li
, Yongxin Zhao
, Geguang Pu^*

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

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

20 Scopus citations

Abstract

Google File System (GFS) is a distributed file system developed by Google for massive data-intensive applications which is widely used in industries nowadays. In this paper, we present a formal model of Google File System in terms of Communicating Sequential Processes (CSP#), which precisely describes the underlying read/write behaviours of GFS. Based on the achieved model some properties like deadlock-free, and consistency model of GFS can be analyzed and verified in the further work.

Original language	English
Title of host publication	Proceedings - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014
Publisher	IEEE Computer Society
Pages	190-191
Number of pages	2
ISBN (Electronic)	9781479964741
DOIs	https://doi.org/10.1109/PRDC.2014.32
State	Published - 3 Dec 2014
Event	20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014 - Singapore, Singapore Duration: 19 Nov 2014 → 21 Nov 2014

Publication series

Name	Proceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC
ISSN (Print)	1541-0110

Conference

Conference	20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014
Country/Territory	Singapore
City	Singapore
Period	19/11/14 → 21/11/14

Keywords

CSP#
Formal Modeling
GFS

Access to Document

10.1109/PRDC.2014.32

Cite this

@inproceedings{83948ee86e52499fb3b4a04c40fd95cb,

title = "Formalizing google file system",

abstract = "Google File System (GFS) is a distributed file system developed by Google for massive data-intensive applications which is widely used in industries nowadays. In this paper, we present a formal model of Google File System in terms of Communicating Sequential Processes (CSP\#), which precisely describes the underlying read/write behaviours of GFS. Based on the achieved model some properties like deadlock-free, and consistency model of GFS can be analyzed and verified in the further work.",

keywords = "CSP\#, Formal Modeling, GFS",

author = "Mengdi Wang and Bo Li and Yongxin Zhao and Geguang Pu",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.; 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014 ; Conference date: 19-11-2014 Through 21-11-2014",

year = "2014",

month = dec,

day = "3",

doi = "10.1109/PRDC.2014.32",

language = "英语",

series = "Proceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC",

publisher = "IEEE Computer Society",

pages = "190--191",

booktitle = "Proceedings - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014",

address = "美国",

}

Wang, M, Li, B, Zhao, Y & Pu, G 2014, Formalizing google file system. in Proceedings - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014., 6974788, Proceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC, IEEE Computer Society, pp. 190-191, 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014, Singapore, Singapore, 19/11/14. https://doi.org/10.1109/PRDC.2014.32

Formalizing google file system. / Wang, Mengdi; Li, Bo; Zhao, Yongxin et al.
Proceedings - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014. IEEE Computer Society, 2014. p. 190-191 6974788 (Proceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC).

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

TY - GEN

T1 - Formalizing google file system

AU - Wang, Mengdi

AU - Li, Bo

AU - Zhao, Yongxin

AU - Pu, Geguang

PY - 2014/12/3

Y1 - 2014/12/3

N2 - Google File System (GFS) is a distributed file system developed by Google for massive data-intensive applications which is widely used in industries nowadays. In this paper, we present a formal model of Google File System in terms of Communicating Sequential Processes (CSP#), which precisely describes the underlying read/write behaviours of GFS. Based on the achieved model some properties like deadlock-free, and consistency model of GFS can be analyzed and verified in the further work.

AB - Google File System (GFS) is a distributed file system developed by Google for massive data-intensive applications which is widely used in industries nowadays. In this paper, we present a formal model of Google File System in terms of Communicating Sequential Processes (CSP#), which precisely describes the underlying read/write behaviours of GFS. Based on the achieved model some properties like deadlock-free, and consistency model of GFS can be analyzed and verified in the further work.

KW - CSP#

KW - Formal Modeling

KW - GFS

UR - https://www.scopus.com/pages/publications/84919478147

U2 - 10.1109/PRDC.2014.32

DO - 10.1109/PRDC.2014.32

M3 - 会议稿件

AN - SCOPUS:84919478147

T3 - Proceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC

SP - 190

EP - 191

BT - Proceedings - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014

PB - IEEE Computer Society

T2 - 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014

Y2 - 19 November 2014 through 21 November 2014

ER -

Formalizing google file system

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this