Formally Verifying the Absence of Overloading in Apache Storm

Apache Storm is widely used for real-time data stream processing in critical domains such as healthcare, logistics, monitoring and enforcement of Internet security, where maintaining performance under high or adversarial workloads is essential. However, modelling it so as to resort to formal verification techniques has proven to be a daunting task. This paper addresses the formal verification of Storm configurations against overloading, expressed as bounded queue growth under given timing and parallelism parameters. We introduce a novel finite-state modelling strategy that preserves essential Storm behaviour, including nondeterministic outputs and timed processing, while abstracting indistinguishable tuples and threads into counters and advancing time by sound leaps between relevant events. The resulting models are generated for NuSMV, hence checked with unbounded symbolic model checking. Experiments on topologies of increasing complexity show that safe configurations are verified without memory exhaustion, and that counterexamples expose unsafe parameter choices.