The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Hackers in Your Pocket: A Survey of Smartphone Security Across Platforms
André Egners, Björn Marschollek, and Ulrike Meyer
AIB 2012-07
In the past research on smart phone operating system security has been
scattered over blog posts and other non-archival publications. Over the
last 5 years with advent of Android, iOS and Windows Phone 7, an
increasing amount of research has also been published in the academic
sphere on individual security mechanisms of the three platfroms.
However, for a non-expert it is hard to get an overview over this
research area.
In this paper, we close this gap and provide a structured easy to access
overview on the security features and prior research of the three most
popular smartphone platforms: Android, iOS, and Windows Phone 7.
In particular, we discuss and compare how each of these platforms uses
sandboxing and memory protection, provides code signing, protects
service connections, provides application shop security, and handles
permissions.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Computing Game Metrics on Markov Decision Processes
Hongfei Fu
AIB 2012-08
In this paper we study the complexity of computing the game bisimulation
metric defined by de Alfaro et al. on Markov Decision Processes. It is
proved by de Alfaro et al. that the undiscounted version of the metric
is characterized by a quantitative game \mu-calculus defined by de
Alfaro and Majumdar, which can express reachability and \omega-regular
specifications. And by Chatterjee et al. that the discounted version of
the metric is characterized by the discounted quantitative game
\mu-calculus. In the discounted case, we show that the metric can be
computed exactly by extending the method for Labelled Markov Chains by
Chen et al. And in the undiscounted case, we prove that the problem
whether the metric between two states is under a given threshold can be
decided in NP and coNP, which improves the previous PSPACE upperbound by
Chatterjee et al.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
dco/c++ - Derivative Code by Overloading in C++
Johannes Lotz, Klaus Leppkes and Uwe Naumann
AIB 2011-06
Algorithmic Differentiation is a widely used technique for computing
derivatives of implemented mathematical functions. In this technical
report we want to introduce the tool dco/c++ written by the authors
implementing Algorithmic Differentiation by Overloading for C/C++. After
a general picture of the capabilities dco/c++ provides, we show its
performance with emphasis on adjoint computations in comparison to four
other freely available overloading tools.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automated Termination Proofs for Java Programs with Cyclic Data
Marc Brockschmidt, Richard Musiol, Carsten Otto, and Jürgen Giesl
AIB 2012-06
In earlier work, we developed a technique to prove termination of Java
programs automatically: first, Java programs are automatically
transformed to term rewrite systems (TRSs) and then, existing methods
and tools are used to prove termination of the resulting TRSs. In this
paper, we extend our technique in order to prove termination of
algorithms on cyclic data such as cyclic lists or graphs automatically.
We implemented our technique in the tool AProVE and performed extensive
experiments to evaluate its practical applicability.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automated Complexity Analysis for Prolog by Term Rewriting
Thomas Ströder, Fabian Emmes, Jürgen Giesl, Peter Schneider-Kamp, and
Carsten Fuhs
AIB 2012-05
For term rewrite systems (TRSs), a huge number of automated termination
analysis techniques have been developed during the last decades, and by
automated transformations of Prolog programs to TRSs, these techniques
can also be used to prove termination of Prolog programs. Very recently,
techniques for automated termination analysis of TRSs have been adapted
to prove asymptotic upper bounds for the runtime complexity of TRSs
automatically. In this paper, we present an automated transformation
from Prolog programs to TRSs such that the runtime of the resulting TRS
is an asymptotic upper bound for the runtime of the original Prolog
program (where the runtime of a Prolog program is measured by the number
of unification attempts). Thus, techniques for complexity analysis of
TRSs can now also be applied to prove upper complexity bounds for Prolog
programs.
Our experiments show that this transformational approach indeed yields
more precise bounds than existing direct approaches for automated
complexity analysis of Prolog. Moreover, it is also applicable to a
larger class of Prolog programs such as non-well-moded programs or
programs using built-in predicates like, e.g., cuts.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Strategy Machines and their Complexity
Marcus Gelderie
AIB 2012-04
We introduce a machine model for the execution of strategies
in (regular) infinite games that refines the standard model
of Mealy automata. This model of controllers is formalized
in the terminological framework of Turing machines. We show
how polynomially sized controllers can be found for Muller
and Streett games. We are able to distinguish aspects of
executing strategies ("size", "latency", "space consumption") that are
not visible in Mealy automata. We show upper and lower bounds
for these parameters for several classes of omega-regular games.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
MontiArc – Architectural Modeling of Interactive Distributed and
Cyber-Physical Systems
Arne Haber, Jan Oliver Ringert, Bernhard Rumpe
AIB 2012-03
This report presents MontiArc, a modeling language for the description
of Component & Connector architectures. A component is a unit executing
computations and/or storing data. Information flow between components is
modeled via unidirectional connectors connecting typed, directed ports
of the interfaces of components.
Language features of the ADL MontiArc include hierarchical decomposition
of components, subtyping by structural inheritance, component type
definitions and reference declarations for reuse, generic component
types and configurable components, syntactic sugar for connectors, and
controlled implicit creation of connections and subcomponent declarations.
This technical report gives an overview of the MontiArc language and is
a reference for the MontiArc grammar intended to enable reuse and
extension of MontiArc and MontiArc related tools.
MontiArc is implemented using the DSL framework MontiCore. Available
tools include an editor with syntax highlighting and code completion as
well as a simulation framework with a Java code generator.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Controlling Development Processes
Thomas Heer
AIB 2012-02
The development of an innovative product is a complex and highly dynamic
process which has to be
performed in a controlled way. Several dependencies exist between the
defined tasks, the assigned
resources, and the artifacts to be produced. In a development project,
which is planned and executed
according to a process definition, the time, budget, and available
resources are limited. Controlling
a development process involves monitoring the actual performance and
analyzing whether it conforms to
the plan. Poor performance, changing requirements, the detection of
errors, and the creation or
modification of key artifacts may require plan changes at process
runtime. As a consequence of the
inherent complexity of the task, software tool support is essential for
controlling development
processes.
Different insufficient solutions are nowadays applied in practice for
this purpose. Project
management systems support project planning and to some degree project
controlling, but they do not
support the execution of predefined processes. Workflow management
systems on the other hand are
commonly applied for process execution. However, they do not support the
scheduling of tasks in a
project, and they are not flexible enough for the management of
development processes. As a
consequence, both types of systems are insufficient when it comes to
controlling development
processes. Attempts for their integration fell short with respect to
representing execution states
in project plans and scheduling workflow instances.
This thesis describes a new concept for a process management system,
which combines the strengths of
the aforementioned tools and eliminates their deficiencies by
substantial extensions. Starting
point of the research were results of the collaborative research center
(SFB) 476 IMPROVE. An
integrated approach for the management of development processes has been
extended with respect to
task scheduling, progress measurement, and change management in
development projects. In
particular, an algorithm for the automatic generation of a project
schedule has been developed
which takes the execution states of the tasks into account. Subprocesses
of a development process
can be executed by a workflow engine, which interprets predefined
workflow definitions. With
respect to monitoring, specific progress measures for the degree of
completion of tasks have been
defined which rely on elements of the process model. In the case of plan
changes at process
runtime, the consistency of the plan with the execution state of the
process is ensured.
The concepts have been implemented in the extension module PROCEED of
the commercial life cycle
asset information management system Comos of Siemens Industry Software.
Comos is widely used in
the plant engineering industries. Therefore, this thesis combines
fundamental research results
with a proof of concept implementation in an industrial context. The
realization of PROCEED based
on an industrial platform offers great opportunities for further
evaluation of the provided
functionalities in plant design projects in the plant engineering
industries.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The Complexity of Deciding a Behavioural Pseudometric on Probabilistic
Automata
Hongfei Fu
AIB 2011-26
In this paper we study the complexity of computing a behavioural
pseudometric on Segala's probabilistic automata. The pseudometric
concerned here stems from a real-valued logic (by Desharnais
\emph{et al}) and does not discount the future. We show that the
problem whether the pseudometric between two states of a finite
probabilistic automata is under a given threshold lies in the
intersection of NP and coNP.
This result significantly improves the previous PSPACE upperbound
(by e.g. van Breugel \emph{et al}).
--
Thomas Ströder mailto:stroeder@informatik.rwth-aachen.de
LuFG Informatik 2 http://verify.rwth-aachen.de/stroeder
RWTH Aachen phone: +49 241 80-21241
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Compiler-Generated Subgradient Code for McCormick Relaxations
Callum Corbett, Michael Maier, Markus Beckers, Uwe Naumann,
Amin Ghobeity, Alexander Mitsos
AIB 2011-25
McCormick Relaxations are special convex and concave under- and
overestimators which are used in the field of nonconvex global
optimization. As they are possibly nonsmooth at some points
subgradients are used as derivative information. Subgradients
are natural extensions of usual derivatives. They may be used to
construct linear or piecewise linear relaxations.
[Mitsos et al. 2009] developed a corresponding method and the
library libMC (written in C++) for propagating relaxations
and related subgradients using the tangent-linear mode of
Algorithmic Differentiation (also known as Automatic
Differentiation) by operator overloading.
This report extends [Mitsos et al. 2009] by providing libMC
functionality by source transformation in Fortran. The
corresponding Fortran module modMC is described. A research
prototype of the NAG Fortran compiler has been extended with
domain-specific inlining techniques to enable the generation of
tangent-linear McCormick code. Speedups by factors of up to four
with respect to the runtime of the respective libMC-based
implementation can be observed. These results are supported by a
number of relevant applications. To perform the numerical
experiments, an interface between tangent-linear McCormick code
written in Fortran and the existing C++-implementation of the
branch-and-bound algorithm has been established.