SpecChecker-Int: An Extensible Concurrency Bugs Detection Tool for Interrupt-driven Embedded Software

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.