Modeling and Verifying Storm Using CSP

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.