arrow
Return

Efficiently Testing Distributed Systems via Abstract State Space Prioritization

delete2025-10-09
delete0
PRE
AI
Y
Yu Gao
D
Dong Wang
窦文生 cover
窦文生 (Wensheng Dou)
W
Wenhan Feng
Y
Yu Liang
J
Jun Wei
DOI:10.1109/TSE.2025.3618976delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

Abstract

En 中文
The last five years have seen a rise of model checking guided testing (MCGT) approaches for systematically testing distributed systems. MCGT approaches generate test cases for distributed systems by traversing their verified abstract state spaces, simultaneously solving the three key problems faced in testing distributed systems, i.e., test input generation, test oracle construction and execution space enumeration. However, existing MCGT approaches struggle with traversing the huge state space of distributed systems, which can contain billions of system states. This makes the process of finding bugs time-consuming and expensive, often taking several weeks. In this paper, we propose Mosso to speed up model checking guided testing for distributed systems. We observe that there exist lots of redundant test scenarios in the abstract state space of distributed systems. Considering the characteristics of these redundant test scenarios, we propose three strategies: action independence, node symmetry and scenario equivalence, to identify and prioritize unique test scenarios when traversing the state space. We have applied Mosso on three real-world distributed systems. By employing the three strategies, our approach has achieved an average speedup of 56X (up to 208X) compared to the state-of-art MCGT approach. Additionally, our approach has successfully uncovered 2 previously-unknown bugs.
Keywords:
Distributed system
model checking
testing

Journal

IEEE Transactions on Software Engineering cover
IEEE Transactions on Software Engineering
IF:
5.6
Papers:
2.9K
Citations:
1.1W

Organization

C
Chinese Academy of Sciences
Scholars:
3.9W
Papers: 1.5W
Citations: 58.4W
Cited Papers

Cited Papers

No cited papers available