AIB 2014-15: Synthesis of State Space Generators for Model Checking Microcontroller Code

[Thomas Ströder]

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Synthesis of State Space Generators for Model Checking Microcontroller Code
Dominique Gückel
AIB 2014-15

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.