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 demonstrates a 30% reduction in detection time. The tool can be found at https://github.com/wangilson/SpecChecker-Int.
Mon 23 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:20 | Bug DetectionResearch Papers / Industry Papers / Demonstrations / Journal First at Aurora B Chair(s): Lingming Zhang University of Illinois at Urbana-Champaign | ||
10:30 20mTalk | Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language Journal First Vikram Nitin Columbia University, Anne Mulhern Red Hat Inc, Sanjay Arora Red Hat Inc, Baishakhi Ray Columbia University | ||
10:50 10mTalk | SpecChecker-Int: An Extensible Concurrency Bugs Detection Tool for Interrupt-driven Embedded Software Demonstrations Boxiang Wang Beijing Sunwise Information Technology Ltd, Chao Li Beijing Institute of Control Engineering; Beijing Sunwise Information Technology, Rui Chen Beijing Institute of Control Engineering; Beijing Sunwise Information Technology, Sheng Wang Beijing Sunwise Information Technology Ltd, Chunpeng Jia Beijing Sunwise Information Technology Ltd, Mengfei Yang China Academy of Space Technology | ||
11:00 20mTalk | dl²: Detecting Communication Deadlocks in Deep Learning Jobs Industry Papers Yanjie Gao Microsoft Research, Jiyu Luo University of Science and Technology of China, Haoxiang Lin Microsoft Research, Hongyu Zhang Chongqing University, Ming Wu Zero Gravity Labs, Mao Yang Microsoft Research DOI Pre-print | ||
11:20 20mTalk | Detecting Metadata-Related Bugs in Enterprise Applications Research Papers Md Mahir Asef Kabir Virginia Tech, Xiaoyin Wang University of Texas at San Antonio, Na Meng Virginia Tech DOI | ||
11:40 20mTalk | ROSCallBaX: Statically Detecting Inconsistencies In Callback Function Setup of Robotic Systems Research Papers Sayali Kate Purdue University, Yifei Gao Purdue University, Shiwei Feng Purdue University, Xiangyu Zhang Purdue University DOI | ||
12:00 20mTalk | Enhancing Web Accessibility: Automated Detection of Issues with Generative AI Research Papers Ziyao He University of California, Irvine, Syed Fatiul Huq University of California, Irvine, Sam Malek University of California at Irvine DOI | ||
Aurora B is the second room in the Aurora wing.
When facing the main Cosmos Hall, access to the Aurora wing is on the right, close to the side entrance of the hotel.