Modeling and Verifying Storm Using CSP

被引：3

作者：

Zhao, Hongyan ^{[1
]}

Zhu, Huibiao ^{[1
]}

Fang, Yucheng ^{[1
]}

Xiao, Lili ^{[1
]}

机构：

[1] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China

来源：

201919TH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING (HASE 2019) | 2019年

关键词：

Storm; CSP; FDR; Formal modeling; Verification;

D O I：

10.1109/HASE.2019.00037

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Due to the higher pursuit of information timeliness, a number of distributed stream processing computation frameworks have emerged, among which the most successful and widely used at present is Storm. Storm is a stream-only processing computation framework which can deal with continuous streaming data. This paper applies Communicating Sequential Processes (CSP), a formal language in process algebra, to analyze and model the communication behaviors in the workflow of Storm. Then, we transform the established model and use the refinement checking tool Failures-Divergences Refinement (FDR) to verify whether it satisfies deadlock-free and sequential consistency properties.

引用

页码：192 / 199

页数：8

共 11 条

[1]

Allen Sean T, 2015, STORM APPL STRATEGIE

[2]

Anderson Q., 2013, Storm real-time processing cookbook: Efficiently process unbounded streams of data in real time

[3]

Apache Software Foundation, 2015, AP STORM DOC

[4]

Fei Yuan, 2018, J SOFTWARE EVOLUTION, V30

[5]

Hoare C.A.R., 1985, Communicating Sequential Processes

[6]

Jain A., 2014, LEARNING STORM

[7]

O'Neill, 2014, STORM BLUEPRINTS PAT

[8]

Requeno J. I., 2017, IEEE INT C INF REUS

[9]

Roscoe AW, 2010, TEXTS COMPUT SCI, P3, DOI 10.1007/978-1-84882-258-0_1

[10] A topology-based scaling mechanism for Apache Storm [J].

Shieh, Ce-Kuen ;

Huang, Sheng-Wei ;

Sun, Li-Da ;

Tsai, Ming-Fong ;

Chilamkurti, Naveen .

INTERNATIONAL JOURNAL OF NETWORK MANAGEMENT, 2017, 27 (03)

← 1 2 →