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 ensure 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 74.83%, highlighting its effectiveness in lowering testing costs for distributed systems.
Wed 25 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | Formal Analysis and Symbolic ExecutionResearch Papers / Tool Demonstrations at Aurora C Chair(s): Na Meng Virginia Tech | ||
16:00 25mTalk | Model Checking Guided Incremental Testing for Distributed Systems Research Papers Yu Gao Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Dong Wang Institute of software, Chinese academy of sciences, Wensheng Dou Institute of Software Chinese Academy of Sciences, Wenhan Feng Institute of Software, Chinese Academy of Sciences, Yu Liang Institute of Software Chinese Academy of Sciences, Yuan Feng Wuhan Dameng Database Co., Ltd, Jun Wei Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences DOI | ||
16:25 25mTalk | Identifying Multi-Parameter Constraint Errors in Python Data Science Library API Documentations Research Papers Xiufeng Xu Nanyang Technological University, Fuman Xie University of Queensland, Chenguang Zhu Meta AI, Guangdong Bai University of Queensland, Sarfraz Khurshid University of Texas at Austin, Yi Li Nanyang Technological University DOI Pre-print | ||
16:50 25mTalk | Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic Research Papers Fanlang Zeng Zhejiang University, Rui Chang Zhejiang University, Hongjian Liu Zhejiang University, Hangzhou, China DOI | ||
17:15 15mDemonstration | TBFV4J: An Automated Testing-Based Formal Verification Tool for Java Tool Demonstrations |
Aurora C is the third room in the Aurora wing.
When facing the main Cosmos Hall, access to the Aurora wing is on the right, close to the side entrance of the hotel.