球友会qy

近期，中国科研实验室软件研究所软件工程技术研究开发中心数据库系统质量保障团队的研究工作取得系列进展，涉及关系型数据库系统在SQL语句和事务执行、图数据库系统查询、分布式数据库系统测试等问题的5篇论文，分别被数据库领域顶级会议VLDB 2025、ICDE 2025和软件工程领域顶级会议ISSTA 2025录用。

在关系型数据库系统SQL语句执行方面，论文Detecting Schema-Related Logic Bugs in Relational DBMSs via Equivalent Database Construction提出了一种基于等价数据库构造（DDLCheck）的SQL正确性检测方法，以有效检测数据库模式演进过程的SQL正确性缺陷。

该方法顺利获得构造复杂的数据定义语言（DDL）序列及其对应的简单DDL序列，创建了两个包含相同数据库模式的等价数据库。对于相同的SQL语句，当等价数据库无法返回相同执行结果时，则表示目标数据库系统产生了一个与数据库模式演进相关的SQL正确性缺陷。此外，研究团队还引入了测试优化策略，来过滤掉重复的DDL序列。基于此方法，研究团队在主流数据库系统（MySQL、PostgreSQL、SQLite、MariaDB、CockroachDB和TiDB）共计发现了34个新缺陷，其中29个得到开发者确认。

DDLCheck流程图

录用会议：VLDB 2025

作者：宋建森、窦文生、郑莹莹、高钰、崔紫玉、王伟、魏峻

链接：http://wsdou.github.io/papers/2025-vldb-ddlcheck.pdf

在关系型数据库系统事务执行方面，论文Simple Testing Can Expose Most Critical Transaction Bugs: Understanding and Detecting Write-Specific Serializability Violations in Database Systems针对现有事务验证工作主要依赖简单数据结构与事务执行历史，而不能支持实际数据库系统中大部分事务特性的局限，提出了一种基于写序列化的数据库事务缺陷自动检测方法WriteCheck。

该方法以并发事务的写序列化特性为基础，即在任何隔离级别下，并发事务执行与特定序列化事务执行产生相同的数据库状态，从而依据并发事务执行调度来推断特定写序列化的调度。当实际事务执行的数据库状态与特定序列化事务执行产生的数据库状态不一致，则表明存在事务缺陷。研究团队顺利获得WriteCheck在六个关系型数据库系统（MySQL、PostgreSQL、SQLite、MariaDB、CockroachDB、TiDB）中，发现了22个特定写序列化违背，其中11个是尚未被披露的新事务缺陷。

WriteCheck流程图

录用会议：VLDB 2025

作者：崔紫玉、窦文生、高钰、杨睿、郑莹莹、宋建森、冯源、魏峻

链接：http://wsdou.github.io/papers/2025-vldb-writecheck.pdf

论文Detecting Isolation Anomalies in Relational DBMSs聚焦关系型数据库系统事务执行的隔离异常问题，提出了一种黑盒隔离检查器IsoRel，以有效识别使用关系数据模型的数据库系统隔离异常，提高隔离级别的准确性，减少触发查询结果错误、数据库状态错误等问题。

IsoRel的核心在于以隔离无关的方式插桩SQL语句，利用数据表中的两个辅助列来记录每个SQL语句访问的数据行。具体来讲，IsoRel在每个数据表中添加rowId辅助列来唯一标识每一行，以及添加wList辅助列来维护创建或修改这一行的事务列表。然后，IsoRel对SQL语句进行插桩，记录并获取每条SQL语句访问的数据行。顺利获得分析并发事务的执行历史，IsoRel推断事务间的写读、写写和读写依赖关系，同时结合隔离异常模式来识别隔离异常。研究团队采用IsoRel，在五个广泛使用的关系型数据库系统（MySQL、PostgreSQL、MariaDB、CockroachDB、TiDB）中，发现了48个违反了Adya定义的隔离级别的隔离异常。

IsoRel流程图

录用会议：ISSTA 2025

作者：杨睿、崔紫玉、窦文生、高钰、宋建森、谢旭东、魏峻

链接：http://wsdou.github.io/papers/2025-issta-isorel.pdf

在图数据库系统查询等价性验证方面，当前证明图查询的等价性往往由经验丰富的开发人员进行人工验证，成本较高且效率较低。为此，论文Proving Cypher Query Equivalence提出了利用代数表达式建模图查询的证明工具GraphQE。

GraphQE将图查询的等价性证明问题转化为代数表达式的等价性证明问题，顺利获得约束求解器实现了图查询等价性的自动化证明。研究团队构建了包含148对等价Cypher查询的验证数据集，GraphQE以平均38m/s的延迟，成功证明了其中的138对，显示出良好的证明能力。

GraphQE流程图

录用会议：ICDE 2025

作者：汤磊、窦文生、郑莹莹、许利杰、王伟、魏峻、黄涛

链接：http://wsdou.github.io/papers/2025-icde-graphqe.pdf

在分布式数据库系统测试方面，研究团队此前在EuroSys 2023上提出了一种模型检查引导的测试方法Mocket，顺利获得形式化模型的抽象状态空间生成测试用例，系统化验证分布式系统的正确性。然而，该方法测试成本较高，尤其在系统演变（如新增功能或修复错误）时，需重新运行全部测试，影响测试效率。

针对上述问题，该研究团队在论文Model Checking Guided Incremental Testing for Distributed Systems提出了一种模型检查引导的分布式系统增量测试方法iMocket，来提高模型检查引导的分布式系统测试效率。该方法从分布式系统形式规范和系统实现中提取系统变化，随后根据提取的系统变化识别抽象状态空间中受系统变化影响的状态，并生成专门针对这些状态的增量测试用例，从而避免对未受影响状态的冗余测试。研究团队在三个主流分布式系统（Raft-java、Xraft和ZooKeeper）对iMocket进行了应用评估。实验表明，iMocket平均能减少74.83%的测试用例数量，并将测试时间降低22.54%至99.99%，显著降低了分布式系统的测试成本。

iMocket流程图

录用会议：ISSTA 2025

作者：高钰、王栋、窦文生、冯文翰、梁堉、冯源、魏峻

链接：http://wsdou.github.io/papers/2025-issta-imocket.pdf

以上研究成果已经在浪潮云溪数据库系统、达梦数据库系统、GaussDB上召开实际应用，并检测出若干真实缺陷。研究取得了国家自然科学基金、中国科研实验室青年创新促进会、中国科研实验室软件研究所创新基金重大项目专项与基础研究项目等的支持。