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 assembly programs became the focus of research projects. It has some advantages compared to model checking programs written in high level programming languages. The code that is deployed to the hardware is checked and not just an intermediate representation. Hence any errors introduced during the complete development process can be found (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 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 and used in a live presentation of the tool. Finally, a conclusion is drawn and some potential future improvements are described.
| Bastian Schlich |
| Rheinisch-Westfälische Technische Hochschule Aachen |
| Date: | Fri Sep 28 2007 |
| Time: | 14:00 to 15:30 |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW Kensington campus |
Last updated by tbourke at Fri Sep 28 12:03:22 2007 GMT+1000