Vortragende(r): Dipl.-Inform. Bastian Schlich
Microcontrollers are frequently used in safety critical systems. Full testing of these systems is often impossible due to fast time to market, uncertain environments, etc. Many companies discovered model checking as a promising future tool for the analysis of such systems. Recently, model checking of assembly programs got into focus of current research projects. It features some advantages compared to model checking of programs written in high level programming languages. The code is checked that is deployed to the hardware and not an intermediate representation. Hence, all errors can be found that are introduced during the complete development process (e.g. compiler errors, errors in handling the hardware, and errors not visible in the C code).
This talk discusses model checking of microcontroller assembly code programs. First, some details about microcontrollers and model checking are given. Then, the advantages and disadvantages of model checking assembly code compared to model checking of C code are described. After that, our model checking tool [mc]square is detailed. The features are itemized, the procedure used is presented, and several details of the architecture are depicted. Next, some abstraction techniques utilized during the model checking process are explained in detail (e.g. dead variable reduction, path reduction and delayed nondeterminism). Subsequently, two programs are introduced which are used in the following live presentation of the tool. In the end, a conclusion is drawn and a couple of potentials for future improvements are described.