Partial Order Reduction Of Bounded Model Checking For Interrupt-driven Systems

Interrupt-driven systems are widely used in safety-critical systems,so the correctness of interrupt-driven system is particularly important.Many interrupt-driven systems are composed of operating system tasks and interrupt handlers.In such systems,the timing and order of interrupts' occurance is quite uncertain.Interrupts occur at different time or in different order may result in different system behaviors.Many design errors in these systems can only be revealed under certain processing sequeces.Therefore,testing is inefficient in the development of interrupt-driven systems.Testing is insufficient to guarantee the correctness of interrupt-driven systems.The appearance of model checking technique makes it possible to analyse and verify the behaviors of interrupt-driven systems comprehensivly.The basic idea of model checking is to use a formalized model to simulate the real system,and then explore the state space of the model exhaustively to determine whether it meets the specifications,taking the advantages of the capability of modern computers.In previous work,we propose a Bounded Model Checking(BMC)method for interrupt-driven systems.The core of this method is to formalize interrupt-driven systems with timed automata and pseudo-code,and then use a depth-first method to explore the state-space.Experiments has proved that this method can effectively detect system errors.But with the growths of number of interrupts,the state-space grows exponentially.As a result,the state-space exploration of large system models become infeasible.Partial Order Reduction(POR)techniques are commonly used to improve efficiency of model checking,which work by eliminating redundant paths that generated by interleavings of independent transitions.After analysing the characteristics of interrupt-driven systems,this paper proposes an optimized Bounded Model Checking algorithm based on a Partial Order Reduction technique.Experiments show that the optimization algorithm can greatly improve the efficiency of model checking for interrupt-driven systems.The main work of this paper is as follows:1.A BMC tool for interrupt-driven system is descripbed in this paper.the interrupt-driven systems are modelled with timed automata and pseudo-code,and the time constrains in the behaviors are modelled as linear inequalities.The SMT(Satisfiability Modulo Theories)Solver Z3 is used to solve the linear inequalities.Experiments has demonstrated that this method can be applied to real interrupt-driven systems,and can effectively detect system errors.2.A complete and practical optimization algorithm which based on Partial Order Reduction technique is proposed.Interrupt events are modelled as transitions of the model.A static analysis technique is used to get the independence relationships between interrupt handlers before verification.In the state exploration process,we generate partial order path according to the dependent relationships when sevaral interrupts' trigger conditions are satisfied.The optimized algorithm executes partial order paths to reach new states.In this way,the optimized algorithm can eliminate redundant paths,therefore reduce the state space,and consequently improve the model-checking efficiency.3.Based on the algorithm above,we developed an impoved model checking tool for interrupt-driven systems.Experimental results show that the proposed optimization algorithm can effectively reduce the state-space and verification time.Moreover,with the increasement of interrupt amount,the effect of our optimization algorithm is more obvious.