Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
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.
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 11:50
|Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote|
|Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote|
Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA)Link to publication DOI Pre-print Media Attached File Attached
|Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson|