Synthesis of State Space Generators for Model Checking Microcontroller Code
Creating software for embedded systems requires rigid quality measures. The reason for this is that errors in the software may have very expensive or even disastrous consequences. This gives rise to the use of formal methods for software verification, such as model checking, theorem proving, and static analysis.
Many embedded systems rely on either application-specific circuits, reconfigurable logics, or microcontrollers. Manufacturers of microcontrollers typically offer a wide variety of devices based on the same core architecture, which are equipped differently and thus offer different functionality. Furthermore, some tool chains exist that allow developers not only to choose from such off-the-shelf devices, but to customize them for specific kinds of tasks. In some cases, this may go to the extent of actually designing new architectures.
It is precisely this wide variety of available devices that complicates the use of automated verification. Tools need to be adapted to a new platform, or even recreated in case they should be implemented in a too hardware-dependent way.
The topic this thesis deals with is the reduction of the necessary effort for adapting a verification tool to new microcontrollers. To this end, we designed a language for describing microcontrollers, SGDL, and a compiler for translating such descriptions into operative simulators and static analyzers. We based our work on [mc]square, which is a platform for model checking and static analysis of assembly code software.
In order to counter the state explosion problem, it is also necessary to include abstractions in generated simulators. We illustrate, on a number of abstraction techniques, how they can be integrated into the approach and whether they can be generated either partly or entirely.
A number of case studies concerning the implementation of simulators with our new language is presented. Additionally, we examine the effectiveness of the aforementioned abstractions that are integrated into the generated simulators, and compare the results to those obtained when using manually implemented simulators.
Many embedded systems rely on either application-specific circuits, reconfigurable logics, or microcontrollers. Manufacturers of microcontrollers typically offer a wide variety of devices based on the same core architecture, which are equipped differently and thus offer different functionality. Furthermore, some tool chains exist that allow developers not only to choose from such off-the-shelf devices, but to customize them for specific kinds of tasks. In some cases, this may go to the extent of actually designing new architectures.
It is precisely this wide variety of available devices that complicates the use of automated verification. Tools need to be adapted to a new platform, or even recreated in case they should be implemented in a too hardware-dependent way.
The topic this thesis deals with is the reduction of the necessary effort for adapting a verification tool to new microcontrollers. To this end, we designed a language for describing microcontrollers, SGDL, and a compiler for translating such descriptions into operative simulators and static analyzers. We based our work on [mc]square, which is a platform for model checking and static analysis of assembly code software.
In order to counter the state explosion problem, it is also necessary to include abstractions in generated simulators. We illustrate, on a number of abstraction techniques, how they can be integrated into the approach and whether they can be generated either partly or entirely.
A number of case studies concerning the implementation of simulators with our new language is presented. Additionally, we examine the effectiveness of the aforementioned abstractions that are integrated into the generated simulators, and compare the results to those obtained when using manually implemented simulators.
