Model Checking Assembly Code of an Industrial Knitting Machine
Thomas Reinbacher, Martin Horauer, Bastian Schlich, Jörg Bräuer, Florian Scheuer · 2009
Microcontrollers are used in many embedded systems. The reliability of these embedded systems is of great importance. Model checking is seen as a promising tool for the analysis of the corresponding software. For this purpose, an on-the-fly CTL model checker for microcontroller assembly code called [MC]SQUARE was developed at the RWTH Aachen University. This paper describes a case study that was conducted using [MC]SQUARE. The aim of the case study was to model check the software of an industrial embedded system used for monitoring a knitting machine without manually modifying the code. Using model checking, we found a bug in the communication protocol of the application that was not revealed during testing.