CLOVER自动化检测中断程序中的原子性违规，提升关键系统可靠性。
Automated detection of atomicity violations in large-scale systems
- 多智能体框架协同静态分析工具生成代码摘要
- 在三个数据集上实现91.0%精确率与96.4%召回率
- 发现11个真实航天项目中的12处未知违规
中断驱动程序中的原子性违规严重威胁安全关键系统的软件可靠性。此类违规源于异步中断破坏了对共享资源的操作执行顺序。由于程序状态空间庞大、应用层代码依赖复杂及领域知识繁复，检测原子性违规极具挑战。本文提出CLOVER，一种用于真实世界中断驱动程序中检测原子性违规的多智能体框架。其规划智能体协调四个静态分析工具提取关键信息并生成代码摘要。随后，CLOVER初始化多个专家-裁判智能体对，以迭代方式检测并验证不同模式的原子性违规。在RaceBench、SV-COMP和RWIP上的评估表明，CLOVER的精确率/召回率为91.0%/96.4%，F1得分优于现有方法33.0-117.2%。此外，它在11个真实航天软件项目中发现了12处原子性违规，其中一处此前未知。
原文摘要 · Abstract (English)
Atomicity violations in interrupt-driven programs pose a significant threat to software reliability in safety-critical systems. These violations occur when the execution sequence of operations on shared resources is disrupted by asynchronous interrupts. Detecting atomicity violations is challenging due to the vast program state space, application-level code dependencies, and complex domain-specific knowledge. In this paper, we propose CLOVER, a multi-agent framework for detecting atomicity violations in real-world interrupt-driven programs. Its plan agent orchestrates four static analysis tools to extract key information and generate code summaries. CLOVER then initializes several Expert-Judge agent pairs to detect and validate different patterns of atomicity violation, through an iterative manner. Evaluations on RaceBench, SV-COMP, and RWIP demonstrate that CLOVER achieves a precision/recall of 91.0%/96.4%, outperforming existing approaches by 33.0-117.2% on F1-score. Additionally, it identifies 12 atomicity violations in 11 real-world aerospace software projects, one of which is previously unknown.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。