Verifying Interrupt-driven Programs Efficiently via Heuristic and Reduced Partial-order Constraints

Abstract

Interrupt-driven programs are extensively utilized in embedded systems for safety-critical domains. However, uncertain interleaving executions of enabled tasks with different priorities often lead to concurrency defects. In this context, assertion violation detection is a fundamental method to ensure program correctness. Worryingly, it remains a challenge for state-of-the-art tools to achieve both precision and efficiency. To address this issue, we introduce a model checking approach for detecting assertion violations in interrupt-driven programs. First, precise partial-order constraints are established to represent potential task interleavings with different priorities. Subsequently, heuristic constraints are formulated to capture the concurrency-control relations inherent in interrupt-driven systems, thereby providing effective guidance for the back-end solver in exploring the solution space. Furthermore, by considering the unique enable-before mechanism specific to interrupt-driven programs, infeasible partial-order constraints are identified and eliminated, resulting in a simplified formula for more efficient reasoning. This formula is finally fed into a modern SAT or SMT solver, along with a constraint specifying the set of error states. Our approach has been implemented in a model checker namely IDPchecker for real-world C programs. Comprehensive experiments demonstrate that the proposed strategies can contribute to the solving time reduction while maintaining enough accuracy, making IDPchecker much more precise and efficient than the relative tools.