| We have been and still are developing a model-checker for microcontroller code called [mc]square at our chair. [mc]square is a CTL model-checker requiring an assember or C program as input. The state space of the model checker is created when executing a program via a simulator of the respective microcontroller (simply stated). [mc]square currently has simulators for Atmel ATmega16 Atmel ATmega128 Intel 8051 Infineon XC167

|

Some of these simulators are the result of diploma theses. In the scope of an industry project, [mc]square is supposed to be used for the verification of a system based on a Renesas microcontroller. Your task is the implementation of the respective simulator.

Implementation of a simulator for a Renesas microcontroller. The definite type of the microcontroller will be determined at the beginning of the familiarization period at the latest. The minimum requirement for the final simulator is the ability to process the instruction set of the microcontroller. Further on-chip periphery is desirable but no mandatory goal.

Implementation of the simulator, application of the model-checker within the industry project.

• Computer science

• Java
• Basic knowledge in microcontroller programming

• rasool

• Dr. rer. nat. Dominique Marcel Gückel