The security problems of software systems caused by integer overflow are common, while the existing model checking techniques have few engineering applications due to the shortcomings of state space explosion and failure to support interrupt-driven program detection. This paper systematically analyzes the distribution and characteristics of integer overflow in aerospace embedded software through some real cases. On the basis of bounded model checking, a program model reduction technique based on integer overflow variable dependence is proposed based on the characteristics of integer overflow variables. At the same time, we present a interference variables dependency sequentialization method for interrupt-driven programs based on the characteristic abstraction of interrupt functions. The results of benchmark programs and real aerospace embedded software experiments show that this method can not only improve the analysis efficiency, but also make the existing model checking techniques applicable to integer overflow detection of the interrupt-driven programs under the premise of guaranteeing the detection rate of integer overflow.