Accelerating Timing Specification Verification of Interrupt-Driven Real-Time Systems

Timing specifications are critical in real-time embedded systems, where even small time deviations may cause system failures. Although designers often model these systems using automata or sequence diagrams, formally verifying their timing properties remains computationally expensive due to the state-space explosion problem. This research proposes an acceleration framework for verifying interrupt-driven real-time systems against explicit clock value timing properties. Using partial order reduction and first-order logic encoding during verification, we abstract certain constructs in the models as parcels to avoid unnecessary state-space exploration. This parcel-based abstraction integrates seamlessly with formal models that support interruption mechanisms. Based on the framework, we implement two acceleration tactics: inclusive and external parcel pruning. Our prototype tool, Parcel, demonstrates the framework's efficacy on both existing models and large-scale models synthesized by LLMs. Experiments show that Parcel significantly improves the verification speed of large-scale, interrupt-driven models, outperforming state-of-the-art tools by thousands of times.