Abstract

Abstract: Embedded systems are ubiquitous in everyday appliances, ranging from washing machines to cars. We present a verification approach for the (often safety-critical) software used in such systems. Embedded systems software is commonly written for specific micro- controller hardware, in a mixture of C with non-standard compiler extensions and assembler. A model checking tool for such software must support features like direct memory accesses, interrupt handling, inline assembler instructions, usage of timers, communication interfaces, etc. In our approach, we first compile a C program to its binary representation with an unmodified standard compiler, disassemble the resulting binary and feed it into our model checking framework. This has the additional benefit of the model checker verifying what is actually executed on the micro-controller and thus may even catch errors introduced during compilation, e.g. in one of the compiler`s optimization passes. We show examples of non- trivial errors that can be found with this approach, and also reflect on its scalability.