Challenges in embedded model checking — a simulator for the [mc]square model checker

Model checking is considered a promising approach for the verification of software for embedded systems. Generating system models that are close to real-life behavior, however, is challenging. As a result, in some approaches a model can be automatically constructed out of the assembly code along with an appropriate target simulator/debugger. The implementation of the latter is crucial for the entire verification process. To that end, this paper presents requirements and challenges that arise when implementing and verifying such a simulator for the [mc]square model checker from the RWTH Aachen University.