一句话：提出模型引导的属性测试，从 MBT 状态出发随机探索并自动合成不变式性质，发现微信支付未知缺陷。
移动支付应用的正确性至关重要，微信支付团队已有的基于模型的 UAT 系统虽能覆盖全部用户操作与业务规则并达到 100% 状态覆盖，但仍存在测试覆盖不足和测试预言预定义两大局限。本文观察到 UAT 测试用例能有效到达所有应用状态，且微信支付存在不变式行为，据此提出模型引导的属性测试方法：从 UAT 发现的状态出发进行随机探索，并依据自动合成的不变式属性验证应用行为，同时设计贪心轨迹缩减算法以压缩失败轨迹。作者实现了 UAT++，在 20,000 机器小时的测试中发现 59 个此前未知缺陷（48 个逻辑缺陷、11 个崩溃缺陷，55 个确认、45 个修复），这些缺陷无法被 UAT 与经典 PBT 发现；状态转移覆盖率较 UAT 和经典 PBT 分别提升 82.6% 与 600.0%，轨迹缩减平均达 79.9%。UAT++ 已部署于微信支付 Android、iOS 与 HarmonyOS 的持续测试流水线。
Ensuring the correctness of mobile payment applications is critical, as even subtle faults can lead to severe financial losses. To ensure reliability, the WeChat Pay (a popular payment app with over one billion active users worldwide) team developed a User Acceptance Testing (UAT) system based on model-based testing (MBT). It maintains use cases specifying user operation sequences and expected app behaviors under business rules. UAT converts these use cases into formal models and generates test cases to validate the app. Although UAT achieves 100% state coverage by covering all user operations and business rules, it still suffers from two major limitations: insufficient test coverage and predefined test oracles. In this paper, we introduce a model-guided property-based testing approach to improving the existing UAT system. We have two key observations: (1) UAT test cases can effectively reach all app states; and (2) WeChat Pay exhibits some invariant behaviors, which can be used to synthesize generic properties for bug finding. Building on these observations, our approach performs random exploration from UAT-discovered states, and validates app behaviors against the automatically synthesized properties. We also propose a greedy trace shrinking algorithm to reduce failure-inducing traces. We implemented our approach as UAT++, an advanced testing tool built upon the UAT system. Across 20,000 machine hours, UAT++ found 59 previously unknown bugs, including 48 logic bugs and 11 crash bugs (55 confirmed, 45 fixed). These bugs could not be found by the UAT system and classic property-base testing (PBT). UAT++ improved state transition coverage by 82.6% and 600.0% over the UAT system and classic PBT, respectively. The shrinking algorithm attained an average trace reduction rate of 79.9%. To date, UAT++ has been deployed in the continuous testing pipeline of WeChat Pay across Android, iOS, and HarmonyOS platforms.
@inproceedings{paperbot12509,
title = {Model-Guided Property-Based Testing of WeChat Pay at Billion-User Scale},
author = {Xiangchen Shen and Yiting Wang and Ting Su and Jingjing Liang and Jingling Sun and Xixian Liang and Haiying Sun and Xinjie Xu and Haochuan Lu and Yuetang Deng and Pengcheng Wang and Geguang Pu and Zhendong Su and John Hughes},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834537}
}