Modeling and Verifying MooseFS in CSP

Yucheng Fang; Huibiao Zhu; Gang Lu; Lili Xiao; Wanling Xie

doi:10.1109/COMPSAC.2018.00043

Modeling and Verifying MooseFS in CSP

Yucheng Fang
, Huibiao Zhu^*
, Gang Lu
, Lili Xiao
, Wanling Xie

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

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

3 Scopus citations

Abstract

Moose File System (MooseFS) is an Open-source, POSIX-compliant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Its high performance, high availability and fault-tolerant features have drawn huge interest from industry. However, the correctness of the dominate parts including reading and writing files of MooseFS has not got much attention of academia, which is the main concern of industry. In this paper, we use the process algebra Communicating Sequential Process (CSP) to model and analyze MooseFS. We mainly focus on the dominant parts which include reading and writing files in MooseFS and formalize them in detail. On that basis, we use the model checker Failures Divergence Refinement (FDR) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties including deadlock freedom, divergence-free, mutual exclusion and backup scheme.

Original language	English
Title of host publication	Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018
Editors	Chung-Horng Lung, Thomas Conte, Ling Liu, Toyokazu Akiyama, Kamrul Hasan, Edmundo Tovar, Hiroki Takakura, William Claycomb, Stelvio Cimato, Ji-Jiang Yang, Zhiyong Zhang, Sheikh Iqbal Ahamed, Sorel Reisman, Claudio Demartini, Motonori Nakamura
Publisher	IEEE Computer Society
Pages	270-275
Number of pages	6
ISBN (Electronic)	9781538626665
DOIs	https://doi.org/10.1109/COMPSAC.2018.00043
State	Published - 8 Jun 2018
Event	42nd IEEE Computer Software and Applications Conference, COMPSAC 2018 - Tokyo, Japan Duration: 23 Jul 2018 → 27 Jul 2018

Publication series

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

Conference

Conference	42nd IEEE Computer Software and Applications Conference, COMPSAC 2018
Country/Territory	Japan
City	Tokyo
Period	23/07/18 → 27/07/18

Keywords

CSP
FDR
Formal methods
MooseFS

Access to Document

10.1109/COMPSAC.2018.00043

Cite this

Fang, Y., Zhu, H., Lu, G., Xiao, L., & Xie, W. (2018). Modeling and Verifying MooseFS in CSP. In C.-H. Lung, T. Conte, L. Liu, T. Akiyama, K. Hasan, E. Tovar, H. Takakura, W. Claycomb, S. Cimato, J.-J. Yang, Z. Zhang, S. I. Ahamed, S. Reisman, C. Demartini, & M. Nakamura (Eds.), Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018 (pp. 270-275). Article 8377667 (Proceedings - International Computer Software and Applications Conference; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/COMPSAC.2018.00043

Fang, Yucheng ; Zhu, Huibiao ; Lu, Gang et al. / Modeling and Verifying MooseFS in CSP. Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018. editor / Chung-Horng Lung ; Thomas Conte ; Ling Liu ; Toyokazu Akiyama ; Kamrul Hasan ; Edmundo Tovar ; Hiroki Takakura ; William Claycomb ; Stelvio Cimato ; Ji-Jiang Yang ; Zhiyong Zhang ; Sheikh Iqbal Ahamed ; Sorel Reisman ; Claudio Demartini ; Motonori Nakamura. IEEE Computer Society, 2018. pp. 270-275 (Proceedings - International Computer Software and Applications Conference).

@inproceedings{0ed2a39fab5a46179201201e472384fb,

title = "Modeling and Verifying MooseFS in CSP",

abstract = "Moose File System (MooseFS) is an Open-source, POSIX-compliant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Its high performance, high availability and fault-tolerant features have drawn huge interest from industry. However, the correctness of the dominate parts including reading and writing files of MooseFS has not got much attention of academia, which is the main concern of industry. In this paper, we use the process algebra Communicating Sequential Process (CSP) to model and analyze MooseFS. We mainly focus on the dominant parts which include reading and writing files in MooseFS and formalize them in detail. On that basis, we use the model checker Failures Divergence Refinement (FDR) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties including deadlock freedom, divergence-free, mutual exclusion and backup scheme.",

keywords = "CSP, FDR, Formal methods, MooseFS",

author = "Yucheng Fang and Huibiao Zhu and Gang Lu and Lili Xiao and Wanling Xie",

note = "Publisher Copyright: {\textcopyright} 2018 IEEE.; 42nd IEEE Computer Software and Applications Conference, COMPSAC 2018 ; Conference date: 23-07-2018 Through 27-07-2018",

year = "2018",

month = jun,

day = "8",

doi = "10.1109/COMPSAC.2018.00043",

language = "英语",

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

publisher = "IEEE Computer Society",

pages = "270--275",

editor = "Chung-Horng Lung and Thomas Conte and Ling Liu and Toyokazu Akiyama and Kamrul Hasan and Edmundo Tovar and Hiroki Takakura and William Claycomb and Stelvio Cimato and Ji-Jiang Yang and Zhiyong Zhang and Ahamed, \{Sheikh Iqbal\} and Sorel Reisman and Claudio Demartini and Motonori Nakamura",

booktitle = "Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018",

address = "美国",

}

Fang, Y, Zhu, H, Lu, G, Xiao, L & Xie, W 2018, Modeling and Verifying MooseFS in CSP. in C-H Lung, T Conte, L Liu, T Akiyama, K Hasan, E Tovar, H Takakura, W Claycomb, S Cimato, J-J Yang, Z Zhang, SI Ahamed, S Reisman, C Demartini & M Nakamura (eds), Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018., 8377667, Proceedings - International Computer Software and Applications Conference, vol. 1, IEEE Computer Society, pp. 270-275, 42nd IEEE Computer Software and Applications Conference, COMPSAC 2018, Tokyo, Japan, 23/07/18. https://doi.org/10.1109/COMPSAC.2018.00043

Modeling and Verifying MooseFS in CSP. / Fang, Yucheng; Zhu, Huibiao; Lu, Gang et al.
Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018. ed. / Chung-Horng Lung; Thomas Conte; Ling Liu; Toyokazu Akiyama; Kamrul Hasan; Edmundo Tovar; Hiroki Takakura; William Claycomb; Stelvio Cimato; Ji-Jiang Yang; Zhiyong Zhang; Sheikh Iqbal Ahamed; Sorel Reisman; Claudio Demartini; Motonori Nakamura. IEEE Computer Society, 2018. p. 270-275 8377667 (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 MooseFS in CSP

AU - Fang, Yucheng

AU - Zhu, Huibiao

AU - Lu, Gang

AU - Xiao, Lili

AU - Xie, Wanling

PY - 2018/6/8

Y1 - 2018/6/8

N2 - Moose File System (MooseFS) is an Open-source, POSIX-compliant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Its high performance, high availability and fault-tolerant features have drawn huge interest from industry. However, the correctness of the dominate parts including reading and writing files of MooseFS has not got much attention of academia, which is the main concern of industry. In this paper, we use the process algebra Communicating Sequential Process (CSP) to model and analyze MooseFS. We mainly focus on the dominant parts which include reading and writing files in MooseFS and formalize them in detail. On that basis, we use the model checker Failures Divergence Refinement (FDR) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties including deadlock freedom, divergence-free, mutual exclusion and backup scheme.

AB - Moose File System (MooseFS) is an Open-source, POSIX-compliant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Its high performance, high availability and fault-tolerant features have drawn huge interest from industry. However, the correctness of the dominate parts including reading and writing files of MooseFS has not got much attention of academia, which is the main concern of industry. In this paper, we use the process algebra Communicating Sequential Process (CSP) to model and analyze MooseFS. We mainly focus on the dominant parts which include reading and writing files in MooseFS and formalize them in detail. On that basis, we use the model checker Failures Divergence Refinement (FDR) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties including deadlock freedom, divergence-free, mutual exclusion and backup scheme.

KW - CSP

KW - FDR

KW - Formal methods

KW - MooseFS

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

U2 - 10.1109/COMPSAC.2018.00043

DO - 10.1109/COMPSAC.2018.00043

M3 - 会议稿件

AN - SCOPUS:85055458208

T3 - Proceedings - International Computer Software and Applications Conference

SP - 270

EP - 275

BT - Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018

A2 - Lung, Chung-Horng

A2 - Conte, Thomas

A2 - Liu, Ling

A2 - Akiyama, Toyokazu

A2 - Hasan, Kamrul

A2 - Tovar, Edmundo

A2 - Takakura, Hiroki

A2 - Claycomb, William

A2 - Cimato, Stelvio

A2 - Yang, Ji-Jiang

A2 - Zhang, Zhiyong

A2 - Ahamed, Sheikh Iqbal

A2 - Reisman, Sorel

A2 - Demartini, Claudio

A2 - Nakamura, Motonori

PB - IEEE Computer Society

T2 - 42nd IEEE Computer Software and Applications Conference, COMPSAC 2018

Y2 - 23 July 2018 through 27 July 2018

ER -

Fang Y, Zhu H, Lu G, Xiao L, Xie W. Modeling and Verifying MooseFS in CSP. In Lung CH, Conte T, Liu L, Akiyama T, Hasan K, Tovar E, Takakura H, Claycomb W, Cimato S, Yang JJ, Zhang Z, Ahamed SI, Reisman S, Demartini C, Nakamura M, editors, Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018. IEEE Computer Society. 2018. p. 270-275. 8377667. (Proceedings - International Computer Software and Applications Conference). doi: 10.1109/COMPSAC.2018.00043

Modeling and Verifying MooseFS in CSP

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this