The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Time-Continuous Behaviour Comparison Based on Abstract Models
Jacob Palczynski
AIB 2013-20
Model-based approaches in the development of embedded software become
more and more widely spread. In these approaches, different models of
one target system are the central elements. Re- cently, a growing number
of algorithms and functionality of embedded software are designed using
such model-based approaches, a prominent one is Rapid Control
Prototyping. Its main advantage is the possibility to develop
functionality of both controlling embedded software and controlled
system in one modelling environment. Additionally, the developer can
simulate the whole system and improve its performance, debug algorithms,
etc. in early development stage. Important test phases are Software in
the Loop and Hardware in the Loop. In this work, we discuss two problems
that may occur during these phases.
The first question is: Taking into account the continuous
characteristics of system variables, how can we safeguard a consistent
evolution of the development artefacts? To deal with this problem, test
results are compared in order to safeguard a consistent evolution of the
development artefacts. Since different artefacts were tested at
different stages of the development under different conditions, we
cannot expect that the results of each test case to be exactly equal,
but at most similar. This similarity check of continuous systems is
addressed in this work.
The methodology presented here is based on behavioural black-box models
of our system in the time domain on different levels of abstraction. A
behaviour is represented by the input and output signals of a system and
their interrelationship. On each level of abstraction, a system’s model
is put up by a set of behaviours, each of which consists of input
signals and the according output signals created by the system. The
description of the signals themselves varies strongly, depending on the
level of abstraction.
For the comparison of two systems or artefacts, we have to introduce a
similarity relation with respect to an abstract model. Two systems are
similar with respect to an abstract model A, when their behaviours
conform to this abstract model A. The central question is how we can
find properties in measured signal data. To find a characteristic
property in a set of measured signal data, we compute the cross
correlation of the interpolated measured data and a template signal. By
this, we find on which time interval of the measured data one property
potentially occurs. Repeating this for all properties yields all
occurrences of the properties in the system’s abstract behaviour model.
In the end, we know that these systems conform the abstract model and
therefore are similar with respect to the abstract model.
The second problem we address is: How can we analyse correctly test
results obtained from real time test devices that do not have certified
clocks? The motivation here are possible differences in sample timing
due to not exactly working hardware timers. Due to this, a drift occurs
in the sampled data which leads to distorted signals and seemingly wrong
timings of events. We compare such a signal to one obtained with a
certified device by searching for certain properties, and obtaining the
points in time of the occurrences. Using these time information, we can
estimate the difference of the sample times, i.e. the drift. For the
search for properties based we use the cross correlation approach
already used for regression tests.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automatic Abstraction for Bit-Vectors using Decision Procedures
Jörg Brauer
AIB 2013-14
This dissertation is concerned with abstract interpretation of programs
whose semantics is defined over finite machine words. Most notably, the
considered class of programs contains executable binary code, the
analysis of which turns out demanding due to the complexity and the
sheer number of involved operations. Challenging for correct yet precise
abstract interpretation of binary code are transfer functions, which
simulate the execution of any concrete operation in a program in an
abstract domain. Crucially for correctness, over- and underflows need to
be supported faithfully.
This dissertation argues that transfer functions and abstractions for
sequences of operations over finite machine words can precisely and
efficiently be generated, which contrasts with classical methods that
depend on handcrafted transfer functions. To support this statement, we
present an approach that eliminates the time-consuming process of
manually deriving transfer functions altogether. The core of our methods
are specifications of the concrete semantics of sequences of operations,
which are given in propositional Boolean logic. By utilizing SAT and SMT
solvers, which can determine satisfiability of Boolean formulae, we show
how to automatically synthesize optimal abstractions from such semantic
specifications. The practicality of our method is highlighted using
abstractions generated for a variety of numerical domains that are
frequently used in abstract interpretation. The abstract domains
considered in this dissertation are, most notably, intervals, value
sets, octagons, convex polyhedra, arithmetical congruences, affine
equalities, and polynomials of bounded degree. Importantly, all
presented techniques automatically handle finiteness of machine words,
which manifests itself in over- and underflows.
Once the analysis of a program has terminated, an abstract interpreter
often emits a warning that highlights a potential error in the analyzed
program. Since abstract interpretation computes an over-approximation of
the states reachable in a concrete execution, such a warning may be
spurious. For this setting, we present variations of our methods, which
compute complete abstractions. Then, it is possible to provide
guarantees about actually reachable states, which allows us to do both,
identify a warning as spurious or generate a legitimate counterexample
trace.