Formal Verification of Preemptive Interrupt-Driven Programs Based on Partial Order Modeling
Junzhe Zhao, Meng Wang, Bin Yu, Zixuan Yuan, Qianchen Yang · 2025
Automated verification of interrupt-driven programs presents significant challenges, as interrupt signals can arrive at arbitrary times and preempt the execution of the current task. This requires considering a vast number of possible execution paths during verification. Furthermore, multiple interrupts may be pending simultaneously, with their service order determined by interrupt priorities. This can lead to nested preemption, further increasing the complexity of the program state space and the difficulty of verification. We propose a formal method based on partial order modeling to verify interrupt-driven programs. Our approach models the interactions among multiple tasks in interrupt-driven programs through partial orders, encoding program execution paths as logical formulas composed of partial order constraints. These formulas are then solved by an SMT solver capable of handling partial order constraints, enabling assertion checking within interrupt-driven programs. We have implemented the proposed method in a prototype tool called DIDP and conducted experiments using a benchmark dataset consisting of real-world embedded system code and device drivers to evaluate its performance. Experimental results demonstrate that, compared to state-of-theart verification tools, DIDP significantly improves verification efficiency while maintaining accuracy.