- tr-announce - lists.rwth-aachen.de

2012-07: Hackers in Your Pocket: A Survey of Smartphone Security Across Platforms
by Thomas Ströder 29 Jun '12

29 Jun '12

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.

1 0

2012-08: Computing Game Metrics on Markov Decision Processes
by Thomas Ströder 31 May '12

31 May '12

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.

1 0

2011-06: dco/c++ - Derivative Code by Overloading in C++
by Thomas Ströder 31 May '12

31 May '12

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.

1 0

2012-06: Automated Termination Proofs for Java Programs with Cyclic Data
by Thomas Ströder 19 Apr '12

19 Apr '12

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.

1 0

2012-05: Automated Complexity Analysis for Prolog by Term Rewriting
by Thomas Ströder 04 Apr '12

04 Apr '12

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.

1 0

2012-04: Strategy Machines and their Complexity
by Thomas Ströder 05 Mar '12

05 Mar '12

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.

1 0

2012-03: MontiArc – Architectural Modeling of Interactive Distributed and Cyber-Physical Systems
by Thomas Ströder 01 Mar '12

01 Mar '12

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.

1 0

2012-02: Controlling Development Processes
by Thomas Ströder 31 Jan '12

31 Jan '12

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.

1 0

2011-26: The Complexity of Deciding a Behavioural Pseudometric on Probabilistic Automata
by Thomas Ströder 23 Dec '11

23 Dec '11

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

1 0

2011-25: Compiler-Generated Subgradient Code for McCormick Relaxations
by Carsten Fuhs 27 Nov '11

27 Nov '11

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.

1 0