Proving Correctness of an Efficient Abstraction for Interrupt Handling

This paper presents an approach to the efficient abstraction of interrupt handling in microcontroller systems. Such systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models, which in turn aggravates the state explosion problem. Careful handling of nondeterminism is therefore crucial for obtaining efficient model checking tools. Here, we support this goal by developing a formal computation model and an abstraction method, called interrupt nondeterminism, which instantiates nondeterministic values only if and when this is required by the application code. It is shown how this symbolic technique can be integrated into our explicit CTL model checking tool [mc]square by introducing lazy states. A lazy state consists of explicit and symbolic parts and therefore, represents several concrete states. With regard to interrupt handling, we also give a simulation relation between the concrete and the abstract state space, thus establishing the correctness of our technique. Furthermore, a case study is presented in which three different programs are used to demonstrate the effectiveness of our method.