Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate

TL;DR

This paper introduces a novel dynamic partial order reduction technique for stateful model checking of non-terminating event-driven applications, significantly reducing search space and enabling analysis of complex, real-world IoT app interactions.

Contribution

It presents the first sound DPOR algorithm for non-terminating, event-driven applications in stateful model checking, addressing a key challenge in verifying such systems.

Findings

Reduced search space for smart home app pairs

Enabled 69 app pairs to complete analysis that previously did not finish

Achieved an average speedup of 7X in model checking

Abstract

Event-driven architectures are broadly used for systems that must respond to events in the real world. Event-driven applications are prone to concurrency bugs that involve subtle errors in reasoning about the ordering of events. Unfortunately, there are several challenges in using existing model-checking techniques on these systems. Event-driven applications often loop indefinitely and thus pose a challenge for stateless model checking techniques. On the other hand, deploying purely stateful model checking can explore large sets of equivalent executions. In this work, we explore a new technique that combines dynamic partial order reduction with stateful model checking to support non-terminating applications. Our work is (1) the first dynamic partial order reduction algorithm for stateful model checking that is sound for non-terminating applications and (2) the first dynamic partial reduction algorithm for stateful model checking of event-driven applications. We experimented with the IoTCheck dataset: a study of interactions in smart home app pairs. This dataset consists of app pairs originated from 198 real-world smart home apps. Overall, our DPOR algorithm successfully reduced the search space for the app pairs, enabling 69 pairs of apps that did not finish without DPOR to finish and providing a 7X average speedup.