Bounded model checking technique for interrupt-driven systems

This paper proposes an approach to model and verify a certain class of interrupt-driven aerospace control systems. These interrupt-driven systems consist of interrupt handlers and system-scheduling tasks. When an interrupt event occurs, the corresponding interrupt-handler executes in response. An interrupt-handler may leave some post-processing works to the system tasks by setting some control variables to certain values. The operating system schedules a set of tasks periodically to deal with routine tasks and some post-processing of interrupt events. In this paper, timed automata labeled with interrupts are used to model interrupt events and task scheduling events. The execution processes of interrupts are modeled by pseudo-code of interrupt handlers and the interrupt vector. Control variables are used to model the interactions between interrupt processing and system tasks while the tasks perform post-processing of interrupts according to the values of control variables set by interrupt handlers. A bounded model checking algorithm is presented in this paper to check these models w.r.t some important timing properties. The algorithm explores all feasible paths in K steps using the depth-first searching method. During the exploring process, time constraints and time requirements in the specification are calculated by the SMT solver Z3. © Copyright 2015, Institute of Software, the Chinese Academy of Sciences. All rights reserved.