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

2016-10: Towards Privacy-Preserving Multi-Party Bartering
by Jera Hensel 20 Dec '16

20 Dec '16

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.

1 0

2016-07: Verification of Programmable Logic Controller Code using Model Checking and Static Analysis
by Jera Hensel 19 Nov '16

19 Nov '16

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.

1 0

2016-09: Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
by Jera Hensel 27 Sep '16

27 Sep '16

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.

1 0

2016-05: Proceedings of the 2nd KuVS Expert Talk on Localization
by Jera Hensel 20 Jul '16

20 Jul '16

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.

1 0

2016-06: The SensorCloud Protocol: Securely Outsourcing Sensor Data to the Cloud
by Jera Hensel 11 Jul '16

11 Jul '16

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.

1 0

2016-04: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
by Jera Hensel 24 Apr '16

24 Apr '16

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.

1 0

2016-03: Lower Runtime Bounds for Integer Programs
by Jera Hensel 12 Apr '16

12 Apr '16

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.

1 0

2016-02: Comparative Evaluation and Improvement of Computational Approaches to, Reachability Analysis of Linear Hybrid Systems
by Jera Hensel 31 Mar '16

31 Mar '16

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.

1 0

2015-13: Ansatz zur variantenreichen und modellbasierten Entwicklung von eingebetteten Systemen unter Berücksichtigung regelungs- und softwaretechnischer Anforderungen
by Jera Hensel 11 Dec '15

11 Dec '15

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.

1 0

2015-14: Symbolic vs. Algorithmic Differentiation of GSL Integration Routines
by Thomas Ströder 11 Nov '15

11 Nov '15

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.

1 0