一句话：提出可扩展工具 SpecChecker-Int，将并发缺陷建模为关键交错序列，并用抢占点选择缩减路径探索空间。
中断驱动嵌入式软件中的并发缺陷普遍且类型多样，可能造成严重安全后果，但现有检测方法往往只针对特定缺陷类型，全面检测成本高，难以在统一框架下覆盖多种并发缺陷。本文提出可扩展的检测工具 SpecChecker-Int：它将各类并发缺陷统一建模为关键交错序列，把缺陷检测问题转化为判定是否存在穿越这些序列的可行并发路径；为提升效率，工具引入抢占点选择策略，显著缩减并发路径的探索空间。作者在基准测试和四个真实航天嵌入式程序上评估该工具，并与现有工具对比。结果表明，SpecChecker-Int 支持更广泛的缺陷类型，检测时间降低约 30%，且工具已开源。
Concurrency bugs in interrupt-driven embedded software are both prevalent and diverse, and can lead to severe safety consequences. However, existing detection methods are often limited to specific types of bug, resulting in high costs for comprehensive detection. Most tools struggle to scale across diverse concurrency bugs within a unified framework. To address these challenges, we propose SpecChecker-Int, an extensible tool for detecting concurrency bugs in interrupt-driven embedded software. SpecChecker-Int models concurrency bugs as critical interleaving sequences and reformulates bug detection as determining whether there exists a feasible concurrent path that traverses these sequences. To improve efficiency, the tool introduces a preemption point selection strategy that significantly reduces the exploration space of concurrent paths. We evaluated SpecChecker-Int on a benchmark and four real-world aerospace embedded programs, and compared it with existing tools. The results show that SpecChecker-Int supports a broader range of bug types and achieves a 30% reduction in detection time. The tool can be found at https://github.com/wangilson/SpecChecker-Int.
DOI 原文 ·
@inproceedings{paperbot9170,
title = {SpecChecker-Int: An Extensible Concurrency Bugs Detection Tool for Interrupt-driven Embedded Software},
author = {Boxiang Wang and Chao Li and Rui Chen and Sheng Wang and Chunpeng Jia and Mengfei Yang},
booktitle = {FSE},
year = {2025},
doi = {10.1145/3696630.3728592}
}