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, h challenging. As a result, in some approaches a model can be is 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.