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.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
HotBox: Testing Temperature Effects in Sensor Networks
Florian Schmidt, Matteo Ceriotti, Niklas Hauser, and Klaus Wehrle
AIB 2014-14
Low-power wireless networks, especially in outside deployments, are
exposed to a wide range of temperatures. The detrimental effect of high
temperatures on communication quality is well known. To investigate
these influences under controlled conditions, we present HotBox, a
solution with the following properties: (1) It allows exposition of
sensor motes to a wide range of temperatures with a high degree of
accuracy. (2) It supports specifying exact spatial orientation of motes
which, if not ensured, interferes with repeatable experiment setups. (3)
It is reasonably easy to assemble by following the information (code,
PCB schematics, hardware list and crafting instructions) available
online, facilitating further use of the platforms by other researchers.
After presenting HotBox, we will show its performance and prove its
feasibility as evaluation platform by conducting several experiments.
These experiments additionally provide further insight into the
influence of temperature effects on communication performance in
low-power wireless networks.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Verifying Probabilistic Systems: New Algorithms and Complexity Results
Hongfei Fu
AIB 2014-16
The content of the dissertation falls in the area of formal verification
of probabilistic systems.
It comprises four parts listed below:
1. the decision problem of (probabilistic) simulation preorder between
probabilistic pushdown automata (pPDAs) and finite probabilistic
automata (fPAs);
2. the decision problem of a bisimilarity metric on finite probabilistic
automata (fPAs);
3. the approximation problem of acceptance probability of
deterministic-timed-automata (DTA) objectives on continuous-time Markov
chains (CTMCs);
4. the approximation problem of cost-bounded reachability probability on
continuous-time Markov decision processes (CTMDPs).
The first two parts are concerned with equivalence checking on
probabilistic automata, where probabilistic automata (PAs) are an
analogue of discrete-time Markov decision processes that involves both
non-determinism and discrete-time stochastic transitions. The last two
parts are concerned with numerical algorithms on Markov jump processes.
In Part 1 and Part 2, we mainly focus on complexity issues; as for Part
3 and Part 4, we mainly focus on numerical approximation algorithms.