Synthesizing simulators for model checking microcontroller binary code

Model checking of binary code is recognized as a promising tool for the verification of embedded software. Our approach, which is implemented in the [MC]SQUARE model checker, uses tailored simulators to build state spaces for model checking. Previously, these simulators have been generated by hand in a time-consuming and error-prone process. This paper proposes a method for synthesizing these simulators from a description of the hardware in an architecture description language in order to tackle these drawbacks. The application of this approach to the Atmel ATmega16 microcontroller is detailed in a case study.