The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Towards Privacy-Preserving Multi-Party Bartering
Stefan Wüller, Ulrike Meyer, and Susanne Wetzel
AIB 2016-10
Both B2B bartering as well as bartering between individuals is
increasingly facilitated through online platforms. However, typically
these platforms lack automation and tend to neglect the privacy of their
users by leaking crucial information about trades. It is in this context
that we devise the first privacy-preserving protocol for automatically
determining an actual trade between multiple parties without involving a
trusted third party.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Verification of Programmable Logic Controller Code using Model Checking
and Static Analysis
Sebastian Biallas
AIB 2016-07
Programmable Logic Controllers (PLCs, ger. Speicherprogrammierbare
Steuerungen) are control devices used in industry to control, operate
and monitor plants, machines and robots. PLCs comprise input
connectors, typically connected to sensors, output connectors, typically
connected to actuators, and a program, which controls the behavior,
computing new output values based on the input values and an internal
state. Since PLCs operate in safety-critical environments, where a
malfunction could seriously harm the environment, humans, or the plant,
it is recommended to verify their programs using formal methods.
This dissertation studies the formal methods model checking and static
analysis to prove the correctness of PLC programs. For this, we
developed the tool ArcadePLC, which allows the automatic application of
these methods to PLC programs written in different vendor-specific
dialects. It extracts a model from the program by abstract simulation,
which over-approximates the possible program behavior. The user is then
able to verify whether the model obeys a specification, which can be
written in the logic CTL or using automata.
For applying model checking, we demonstrate how the model can be
extracted automatically, such that the approach scales to industrial
size programs. For this, we introduce two different abstraction
techniques: First, we develop an abstraction refinement guided by the
model checker that automatically creates an abstracted model by
iteratively analyzing counterexamples. Second, we implemented a
predicate abstraction that evaluates a formalized program semantics
using an SMT solver. Both techniques are evaluated using different
programs from industry and academia. Further, we introduce a simplified
formalism to write specifications, which is influenced by an
automata-based language established in industry. We implement an
algorithm to check programs using this formalism and show that this
technique is even able to detect errors in the specification. Finally,
we detail how counterexamples generated by the model checker can be
analyzed automatically to locate the actual erroneous line in the program.
The static analysis we developed is able to detect program errors in a
fully automatic way. We detect typical errors such as division by zero
and illegal array accesses, but also PLC specific errors, e.g., during a
restart. The analysis is based on a value-set analysis, which
determines the values of all program variables in each program
location. These sets are then verified against the predefined checks or
user-provided annotations. We show how to implement this analysis such
that it scales to industrial size programs. The approach is evaluated on
an industrial case study.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automatically Proving Termination and Memory Safety for Programs with
Pointer Arithmetic
Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten
Fuhs, Jera Hensel, Peter Schneider-Kamp, and Cornelius Aschermann
AIB 2016-09
While automated verification of imperative programs has been studied
intensively, proving termination of programs with explicit pointer
arithmetic fully automatically was still an open problem. To close this
gap, we introduce a novel abstract domain that can track allocated
memory in detail. We use it to automatically construct a symbolic
execution graph that over-approximates all possible runs of a program
and that can be used to prove memory safety. This graph is then
transformed into an integer transition system, whose termination can be
proved by standard techniques. We implemented this approach in the
automated termination prover AProVE and demonstrate its capability of
analyzing C programs with pointer arithmetic that existing tools cannot
handle.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Proceedings of the 2nd KuVS Expert Talk on Localization
Mathias Pelka, Grigori Goronzy, Jó Agila Bitsch, Horst Hellbrück, and
Klaus Wehrle (Editors)
AIB 2016-05
Localization is a key technology in the field of medical, industrial and
logistics applications. Especially indoor applications benefit from
localization, e.g. the knowledge, where personnel is required, scarce
resources are available, and goods move. Similarly, autonomous vehicles
require reliable localization information for a wide range of tasks.
Localization information saves time and money and can also save lives in
case of emergency. However, there is no generic solution in near future
that will cover all use cases and all environments.
With the 2nd Expert Talk on Localization we provide a forum for the
presentation and discussion of new research and ideas in a local
setting, bringing together experts and practitioners from academia and
industry. As a result, a considerable amount of time is devoted to
informal and moderated discussions, for instance during the extended
breaks. In addition to traditional localization topics such as radio
based localization, we also aim at novel technologies by encouraging
submissions offering research contributions related to algorithms,
stability and reliability, and applications. The high-quality program
includes numerous contributions, starting with UWB range-based radio
technology approaches, topological simplifications and clustering
schemes, as well as automotive applications, together with visual
localization approaches and fundamental limits of localization.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The SensorCloud Protocol: Securely Outsourcing Sensor Data to the Cloud
Martin Henze, René Hummen, Roman Matzutt, and Klaus Wehrle
AIB 2016-06
The increasing deployment of sensor networks, ranging from home networks
to industrial automation, leads to a similarly growing demand for
storing and processing the collected sensor data. To satisfy this
demand, the most promising approach to date is the utilization of the
dynamically scalable, on-demand resources made available via the cloud
computing paradigm. However, prevalent security and privacy concerns are
a huge obstacle for the outsourcing of sensor data to the cloud. Hence,
sensor data needs to be secured properly before it can be outsourced to
the cloud.
When securing the outsourcing of sensor data to the cloud, one important
challenge lies in the representation of sensor data and the choice of
security measures applied to it. In this paper, we present the
SensorCloud protocol, which enables the representation of sensor data
and actuator commands using JSON as well as the encoding of the object
security mechanisms applied to a given sensor data item. Notably, we
solely utilize mechanisms that have been or currently are in the process
of being standardized at the IETF to aid the wide applicability of our
approach.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Proving Termination of Programs with Bitvector Arithmetic by Symbolic
Execution
Jera Hensel, Jürgen Giesl, Florian Frohn, and Thomas Ströder
AIB 2016-04
In earlier work, we developed an approach for automated termination
analysis of C programs with explicit pointer arithmetic, which is based
on symbolic execution. However, similar to many other termination
techniques, this approach assumed the program variables to range over
mathematical integers instead of bitvectors. This eases mathematical
reasoning but is unsound in general. In this paper, we extend our
approach in order to handle fixed-width bitvector integers. Thus, we
present the first technique for termination analysis of C programs that
covers both byte-accurate pointer arithmetic and bit-precise modeling of
integers. We implemented our approach in the automated termination
prover AProVE and evaluate its power by extensive experiments.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Lower Runtime Bounds for Integer Programs
Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen
Giesl
AIB 2016-03
We present a technique to infer lower bounds on the worst-case runtime
complexity of integer programs. To this end, we construct symbolic
representations of program executions using a framework for iterative,
under-approximating program simplification. The core of this
simplification is a method for (under-approximating) program
acceleration based on recurrence solving and a variation of ranking
functions. Afterwards, we deduce asymptotic lower bounds from the
resulting simplified programs. We implemented our technique in our tool
LoAT and show that it infers non-trivial lower bounds for a large number
of examples.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Comparative Evaluation and Improvement of Computational Approaches to
Reachability Analysis of Linear Hybrid Systems
Ibtissem Ben Makhlouf
AIB 2016-02
This thesis addresses the problem of reachability analysis with the focus
on linear hybrid systems. Hybrid systems are a mixture of continuous
and discrete behaviors. The Hybrid automaton consisting of a graph,
in which the locations describe the continuous and the transitions
the discrete behavior, represents the best formal model for such kind
of systems. It provides a formalism integrating differential equations
and logic expressions in a same framework, thus opening new horizons in
research and development of new methods and novel algorithms. Despite
recent progress made in this field in the last years, actual verification
methods and available tools have exhibited their shortcomings.
We started this work with the assessment of some verification tools
using a suite of benchmarks conceived specially for this task. The
benchmarks possess particular characteristics for testing of efficiency,
applicability, scalability, capability and performances of these tools.
We offer a theoretical overview of existing methods for computing an
overapproximation of reachable sets for linear time invariant hybrid
systems. This covers approaches for overapproximating reachable sets of
the continuous dynamics with and without invariants as well as methods for
solving the problem of guard intersection at transitions. We furthermore
propose new overapproximation techniques for treating the continuous
part as well as the discrete part of the hybrid automaton. We suggest
scalable, modular implementations of these diverse methods allowing
thereby possible combinations between them first using support functions
and then with zonotopes. The implementations include different approaches
for handling invariants, guards and transitions for the above-mentioned
set representations. Two toolboxes are the results of this implementation
effort. Both tools integrate the methods described above. They offer a
GUI and allow for a user-configurable reachability analysis. We use both
tools to carry out a performance comparison of different methods. We
note thereby that there is a correlation between these performances
and the complexity of the tested example. However, we note during this
survey using the proposed benchmark suite that the difference in the
performance with regards to the tightness of the over-approximation and
the computation time is not so crucial for low dimensional systems.
We propose a networked platoon of vehicles to demonstrate different
context where reachability analysis can be useful. We first perform
a reachability analysis to determine unsafe gaps between the vehicles
which are controlled using LMI-formalism. Reachability analysis can be
helpful for control design. The choice between controllers on the basis of
reachability results has led to controller ensuring the best compromise
between safe and small gaps when applying H2 or H∞ control design
techniques. Reachability can also be used to determine time-critical
conditions. As demonstration, we opt for a platoon approaching an
intersection.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Ansatz zur variantenreichen und modellbasierten Entwicklung von
eingebetteten Systemen unter Berücksichtigung regelungs- und
softwaretechnischer Anforderungen
Andreas Polzer
AIB 2015-13
Nowadays, model-based development is a common method to deal with the
complexity and wide rages of functionality in embedded systems.
Especially in automotive domain MATLAB/Simulink is often used to develop
controller software for embedded systems. However the usually used tools
are originally not designed to model a product-line of embedded systems
applications. Therefore there is a high complexity of the designed
models. Additionally different tools are used for different design
artefacts like requirements and implementation model. These tools are
not connected to each other's which causes inconsistencies.
Different domains like electrical engineers, control engineers and
computer scientist are involved in designing embedded systems. The
different domains use different domain specific languages and have
different requirements.
This thesis introduces an approach considering requirements of different
domains designing embedded systems. The main focus is the further
model-based development of existing embedded applications, in particular
the cooperation of control engineering and computer science. Both
domains have partly different requirements. E. g. in computer science it
is important to reuse software. However in control engineering there is
a need for great flexibility in terms of external interface (actuators
and sensors) and the according software parts since the actuators and
sensor have critical influence on the performance of the controller.
Hence both domains have conflicting requirements.
In the second part of this thesis an approach on software product-line
is adopted to the model-based development process. Model-based
transformations and analysis are used to support the development. The
transformations use all design artefacts to achieve consistent models
with respect derived variants. The result of the analysis are views.
This views are implemented using standardized transformations provided
by a framework. Therefore new analysis views can be created combining
and adopting these transformations.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Symbolic vs. Algorithmic Differentiation of GSL Integration Routines
Niloofar Safiran and Uwe Naumann
AIB 2015-14
Forward and reverse modes of algorithmic differentiation (AD) transform
implementations of multivariate vector functions as computer programs
into tangent and adjoint code, respectively. The adjoint mode is of
particular interest in large-scale functions due to the independence of
its computational cost on the number of free variables. The additional
memory requirement for the computation of derivatives of the output with
respect to parameters by a fully algorithmic method (derived by AD) can
quickly become prohibitive for large values of n. This can be reduced
significantly by the symbolic approach to differentiation of the
underlying integration routine. Vectorizing gsl routines for integration
and applying symbolic adjoint on them has considerably less memory
requirement with nearly the same runtime overhead and in most cases
faster convergence in comparison with algorithmic adjoint.