Model Checking Guided Incremental Testing for Distributed Systems

Recently, model checking guided testing (MCGT) approaches have been proposed to systematically test distributed systems. MCGT automatically generates test cases by traversing the entire verified abstract state space derived from a distributed system’s formal specification, and it checks whether the target system behaves correctly during testing. Despite the effectiveness of MCGT, testing a distributed system with MCGT is often costly and can take weeks to complete. This inefficiency is exacerbated when distributed systems evolve, such as when new features are introduced or bugs are fixed. We must re-run the entire testing process for the evolved system to verify its correctness, rendering MCGT not only resource-intensive but also inefficient. To reduce the overhead of model checking guided testing during distributed system evolution, we propose iMocket, a novel model checking guided incremental testing approach for distributed systems. We first extract the changes from both the formal specification and system implementation. We then identify the affected states within the abstract state space and generate incremental test cases that specifically target these states, thereby avoiding redundant testing of unaffected states. We evaluate iMocket using 12 real-world change scenarios drawn from three popular distributed systems. The experimental results demonstrate that iMocket can reduce the number of test cases by an average of 74.83% and decrease testing time by 22.54% to 99.99%. This highlights its effectiveness in lowering testing costs for distributed systems.