Modeling and verifying storm using CSP

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019
EditorsVu Nguyen, Dongjin Yu, Congfeng Jiang
PublisherIEEE Computer Society
Pages192-199
Number of pages8
ISBN (Electronic)9781538685402
DOIs
StatePublished - 22 Mar 2019
Event19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019 - Hangzhou, China
Duration: 3 Jan 20195 Jan 2019

Publication series

NameProceedings of IEEE International Symposium on High Assurance Systems Engineering
Volume2019-January
ISSN (Print)1530-2059

Conference

Conference19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019
Country/TerritoryChina
CityHangzhou
Period3/01/195/01/19

Keywords

  • Csp
  • Fdr
  • Formal modeling
  • Storm
  • Verification

Fingerprint

Dive into the research topics of 'Modeling and verifying storm using CSP'. Together they form a unique fingerprint.

Cite this