Refining assembly code static analysis for the Intel MCS-51 microcontroller

Embedded systems are ubiquitous and their software is in most cases the elaborate part of the system. The use of formal verification methods such as model checking was proposed to verify these software systems. One disadvantage of model checking is that it suffers from the state-explosion problem. [mc]square combines model checking and static source code analysis at assembly code level to alleviate this downside. This approach allows considering particular features of the targeted microcontroller. In this paper, a novel data-flow analysis termed register bank analysis is presented. This analysis is an extension of a reaching definitions analysis to cope with register bank switching as performed by the Intel MCS-51 target. An informal and a formal description of the register bank analysis is given and an example to highlight the effectiveness of our approach is presented. Moreover, four remaining challenges in assembly code static analysis are pointed out.