Modeling And Verification For Embedded Interrupt Based On Extended Time Petri Nets

Embedded systems achieve interactions with peripherals and environment through the interrupt mechanism. However, due to the preemptive execution, response with priority, and randomness of trigger method, interrupt behaviors are hard to accurately predict and difficult to track. Interrupt-driven systems need high quality tests, but there is lack of effective detection method for interrupt system at present. This work studies modeling and verification methods of the embedded interrupt system, focusing on the difficult modeling problems for interrupt behavior and creditability validation of interrupt system software.A modeling method of embedded interrupt system is proposed based on extended time Petri nets. Firstly, the formal semantics and modeling capabilities of traditional time Petri nets are extended by defining three different types of migration to simulate hierarchical design and interrupt behaviors of embedded systems, which can effectively model the concurrency, time series, nesting of interrupt and other complex interrupt behaviors. Then, the modeling concept of hierarchical interruptible time Petri nets(HITPN) is first introduced in this paper, whose modeling capability is applied and analyzed through the design of three different types of interrupt behavior scenarios.Three different methods for the analysis and verification are proposed based on HITPN model of embedded interrupt system. Firstly, the reachability graph construction algorithm and analysis methods are proposed for HITPN model. Secondly, the HITPN is transformed into timed automata model, which can be combined with UPPAAL to complete the model checking for embedded systems. Thirdly, a symbolic encoding approach is investigated to formalize the timed automata model and invariant properties, through which the timed automata could be bounded model checked by using the Satisfiability Modulo Theories (SMT) solving technique. Finally, the experimental results demonstrate the effectiveness of the proposed methods, which realized the credibility verification and performance evaluation of interrupt-driven embedded systems in one model from different angles.