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

2015-12: Tree-like Grammars and Separation Logic
by Thomas Ströder 23 Sep '15

23 Sep '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Tree-like Grammars and Separation Logic Christoph Matheja, Christina Jansen, and Thomas Noll AIB 2015-12 Separation Logic with inductive predicate definitions (SL) and hyperedge replacement grammars (HRG) are established formalisms to describe the abstract shape of data structures maintained by heap-manipulating programs. Fragments of both formalisms are known to coincide, and neither the entailment problem for SL nor its counterpart for HRGs, the inclusion problem, are decidable in general. We introduce tree-like grammars (TLG), a fragment of HRGs with a decidable inclusion problem. By the correspondence between HRGs and SL, we simultaneously obtain an equivalent SL fragment (SLTL) featuring some remarkable properties including a decidable entailment problem.

1 0

2015-11: Information Hiding in the Public RSA Modulus
by Thomas Ströder 15 Jun '15

15 Jun '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Information Hiding in the Public RSA Modulus Stefan Wüller, Marián Kühnel, and Ulrike Meyer AIB 2015-11 The manufacturer of an asymmetric backdoor for a public key cryptosystem manipulates the key generation process in such a way that he can extract the private key or other secret information from the user's public key by involving his own public/private key pair. All backdoors in major public key cryptosystems, including RSA, differ substantially in their implementation approaches and in their quality in satisfying backdoor related properties like confidentiality or concealment. While some of them meet neither of these two properties very well, others provide a high level of confidentiality but none of them is concealing, which limits their use for covert implementation. In this work we introduce two novel asymmetric RSA backdoors, both following the approach to embed bits of one of the RSA prime factors in the user's public RSA modulus. While our first backdoor provides confidentiality for a sufficiently large key length, it might be detected under certain circumstances. The second backdoor extends the first one such that it additionally provides concealment and is thus particularly suitable for covert implementation.

1 0

2015-02: Testing Life Cycle-related Properties of Mobile Applications
by Thomas Ströder 10 May '15

10 May '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Testing Life Cycle-related Properties of Mobile Applications Dominik Franke AIB 2015-02 With an increasing number of mobile devices like smartphones and tablets, their relevance to users and growing number of available applications, also their field of application widens. For the software quality of mobile applications, the application life cycle - the process-related states and state transitions - plays an important role. Today's mobile platforms, like Android, iOS and Windows Phone, have specific scheduling policies on application level to ensure the reactiveness of an application, targeting an improved responsiveness and a good user experience. Depending on the life cycle state of an application, it is allowed or restricted to access resources like RAM and CPU. Such policies can lead to data loss and unexpected behavior of the mobile application. This work presents a conceptual approach for testing application properties which are related to life cycle state changes, so called life cycle-related properties. The first step consists of reverse engineering the life cycles of mobile applications. These life cycles are used as a basis for testing life cycle-related properties at state changes. The testing approach uses callback-mechanisms of the underlying mobile platforms to check assertions about life cycle-related properties. It handles application components with an own life cycle as units and tests each unit in a unit-based testing approach. In a case study, the conceptual approach is implemented for the mobile platform Android. One of the results of the case study is the AndroLIFT tool for testing life cycle-related properties of Android applications. The evaluation of this work presents the capabilities and limitations of the conceptual approach. While the approach is well-suited for today's mobile platforms, extensible and scalable with respect to the type and number of life cycle-properties, it mainly depends on the callback-mechanism of the underlying mobile platform. The evaluation of the AndroLIFT tool in the context of a practical course with student participants confirms the value of the Android implementation of the presented approach to test life cycle-related properties of Android applications.

1 0

2015-08: Proceedings of the 1st KuVS Expert Talk on Localization
by Thomas Ströder 05 May '15

05 May '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Proceedings of the 1st KuVS Expert Talk on Localization Mathias Pelka, Jó Agila Bitsch, Horst Hellbrück, and Klaus Wehrle (Editors) AIB 2015-08 Localization has become a major key technology in the field of medical, industrial and logistics applications. Especially indoor applications can benefit, e.g. the knowledge, where personnel are required, scarce resources are scattered, and goods are moving. Similarly, autonomous vehicles require reliable localization information for a wide range of task. Localization information in such places can save lives, time and money. However, there is no overall easy solution that covers all use cases. With the 1st GI Expert Talk on Localization we aim to provide a forum for the presentation and discussion of new research and ideas in a local setting, bringing together experts and practitioners. As a result, a considerable amount of time is devoted to informal discussion. In addition to traditional localization topics such as radio based localization, we also aimed at novel technologies by encouraging submissions offering research contributions related to algorithms, stability and reliability, and applications. As a result the program includes a diverse set of contributions, ranging from phase and range based radio technology approaches, topological simplifications and clustering schemes, as well as automotive applications, including visual localization approaches.

1 0

2015-07: Experimental Validation and Mathematical Analysis of Cooperative Vehicles in a Platoon
by Thomas Ströder 15 Apr '15

15 Apr '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Experimental Validation and Mathematical Analysis of Cooperative Vehicles in a Platoon Hilal Diab AIB 2015-07 The infrastructure of roads in many countries is congested because of the rapid increase of the amount of traffic flow in the past few years. A significant part of this is due to the increase of freight transport, which is continuing to grow. Nowadays, safety on the roads and saving fuel should also be taken into consideration while finding the solutions to road congestion. One suggested solution to the problem is to increase the capacity of the highways. This can be realized by forming platoons of vehicles and automatically controlling the vehicles in order to maintain short, but at the same time, safe distances between the different vehicles within the platoon. The development of intelligent sensors and electronic control systems within vehicles make autonomous driving in platoons possible. Enabling vehicular wireless communication between the items of the platoon improves the performance of the controlled platoon significantly. Furthermore, enabling the platoon to communicate with other traffic members, such as other vehicles, intelligent traffic lights and infrastructure road units, allows the platoon to perform more complex driving scenarios for autonomous vehicles, such as crossing intersections. The first part of this thesis investigates the behavior of the platoon when only communication between its items is possible. The safety of the vehicles within the platoon is investigated, taking the effects of the communication faults on the behavior into account. This analysis could be helpful in the process of controller design, where the developed controller should ensure stability despite network failures and should achieve an optimal performance in every situation. Therefore, the verification of the controller behavior was investigated by formal verification methods: a reachability analysis of a dynamic and hybrid system. The safety of practical relevant scenarios was checked. In addition, a hardware platform was set up to test the platoon's behavior under the influence of hardware shortage, such as noises and time delays caused by hardware components. A 1:14 scaled platoon of four trucks equipped with sensors and WiFi modules was designed. This platform was used for testing different cooperative vehicle platoon controllers by examining their performance and influence on the safety in case of communication problems within the platoon. The second part of this thesis studies the behavior of the platoon when communication between the platoon and the intersection road unit is enabled. The following scenario has been considered: When a platoon of autonomous vehicles following a leader approaches an intersection, the platoon should change its highway mode to other modes in order to cross the intersection safely and efficiently. To realize that, information about the actual position of the platoon together with information of other vehicles in the intersection area are needed. Based on this information the platoon has to decide which mode should be performed. Therefore, we extended our platform with an indoor positioning system which is able to provide the position to the objects in a test environment independently. An intersection management system was implemented in order to test different scenarios related to different crossing modes of the platoon. Results showed that platoons can be controlled efficiently and safely while crossing the intersection.

1 0

2015-09: Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models
by Thomas Ströder 08 Apr '15

08 Apr '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models Xin Chen AIB 2015-09 With the ubiquitous use of computers in controlling physical systems, it requires to have a new formalism that could model both continuous flows and discrete jumps. Hybrid systems are introduced to this purpose. A hybrid system, which is modeled by a hybrid automaton in the thesis, is equipped with finitely many discrete modes and continuous real-valued variables. A state of it is then represented by a mode along with a valuation of the variables. Given that the system is in a mode l, the variable values are changed continuously according to the Ordinary Differential Equation (ODE) associated to l, or discretely by a jump starting from l. The thesis focuses on the techniques to compute all reachable states over a bounded time horizon and finitely many jumps for a hybrid system with non-linear dynamics. The results of that can then be used in safety verification of the system. Although a great amount of work has been devoted to the reachability analysis of hybrid systems with linear dynamics, there are few effective approaches proposed for the non-linear case which is very often in applications. The difficulty is twofold. Firstly, it is not easy to find an over-approximation with acceptable accuracy for a set of the solutions of a non-linear ODE. Secondly, to detect and compute the reachable states under a jump requires solving non-linear real arithmetic problems which is also difficult in general. In the thesis, we present our approaches to deal with the above difficulties. For the first one, we present the use of Taylor models as the over-approximate representations for non-linear ODE solutions. Our work can be viewed as a variant of the Taylor model method proposed by Berz et al., such that we are able to efficiently deal with some examples with more than $10$ variables. Besides, we also extend the work of Lin and Stadtherr to handle the ODEs with bounded time-varying parameters. For the second difficulty, we present two techniques: (a) domain contraction and (b) range over-approximation to compute an enclosure for the reachable set from which a jump is enabled. They can be seen as Satisfiability Modulo Theories (SMT) solving algorithms which are specialized for the reachability analysis of hybrid systems. In order to reduce the computational cost, we also propose different heuristics for aggregating Taylor models. Besides the above contributions, we describe a method to fast generate Taylor model over-approximations for linear ODE solutions. Its performance is demonstrated via a comparison with the tool SpaceEx. To make our methods accessible by other people, we implement them in a tool named Flow*. To examine the effectiveness, we thoroughly compare it with some related tools which are popularly used, according to their functionalities, over a set of non-trivial benchmarks that are collected by us from the areas of mechanics, biology, electronic engineering and medicine. From the experimental results, the advantage of Flow* over the other tools becomes more apparent when the scale of the system grows. On the other hand, it also shows that Flow* can be applied to analyzing realistic systems.

1 0

2013-16: Java Program Analysis by Symbolic Execution
by Thomas Ströder 25 Mar '15

25 Mar '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Java Program Analysis by Symbolic Execution Carsten Otto AIB 2013-16 Program analysis has a long history in computer science. Even when only considering the important aspect of termination analysis, in the past decades an overwhelming number of different techniques has been developed. While the programming languages considered by these approaches initially were more of theoretical importance than of practical use, recently also automated analyses for imperative programming languages like C or Java have been developed. Here, a major challenge is to deal with language constructs and concepts which do not exist in simpler languages. For example, in Java one often uses dynamic dispatch, complex object hierarchies, or side-effects with far-reaching consequences involving the global heap. In this thesis, we present a preprocessing step for JBC programs in which all such complicated language constructs are handled. This way, subsequent analyses do not need to be concerned with these, and making use of existing techniques is easy. In particular, we show how Symbolic Execution Graphs can be constructed which contain an over-approximation of all possible program runs. This way, and by taking care of having a precise approximation, the information contained in the constructed graphs can, for example, be used to reason about the termination behavior of the original program. Additionally to the construction of such graphs, in this thesis we present a new analysis technique which helps end users identify parts of the analyzed code which are irrelevant for the desired outcome. This way, programming errors causing code to be not executed can be identified and, consequently, fixed by the user. For this technique to be useful, the information contained in the previously constructed graph needs to be precise. We will demonstrate that this is the case. For the techniques presented in this thesis, a rigorous formalization is shown. To comply with the overall goal of, for example, automated termination analysis, we also need to implement the techniques and theoretical results. In this thesis we show how certain hard to automate aspects can be approached, leading to a competitive implementation. The techniques presented in this thesis are implemented in the AProVE tool. As also related techniques working on Symbolic Execution Graphs are implemented in AProVE, with the click of a button users can analyze JBC programs for (non)termination and find irrelevant code. In the annual International Termination Competition, it is demonstrated that currently AProVE is the most powerful termination analyzer for JBC programs.

1 0

2015-06: Proceedings of the Young Researchers' Conference "Frontiers of Formal Methods"
by Thomas Ströder 19 Feb '15

19 Feb '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Proceedings of the Young Researchers' Conference "Frontiers of Formal Methods" Thomas Ströder and Wolfgang Thomas (Editors) AIB 2015-06 The Young Researchers' Conference "Frontiers of Formal Methods" (FFM 2015) is a "singularity" - an event that is not part of a longer conference series, but organized following a nice coincidence of interests of several research groups in Germany and Austria. It all started with a loose promise given in 2010: When the second phase of the DFG research training group (Graduiertenkolleg) "AlgoSyn" started in Aachen, we promised to organize a final conference at the end of altogether nine successful years of work by and with doctoral students. In discussions between the speakers of closely related research training groups, it became then clear that all our doctoral students would gain most by a jointly organized conference. Five partners joined their forces: the DFG research training groups AlgoSyn (Algorithmic Synthesis of Reactive and Discrete-Continuous Systems), Aachen, PUMA (Program and Model Analysis), Munich, QuantLA (Quantitative Logics and Automata), Dresden & Leipzig, SCARE (System Correctness under Adverse Conditons), Oldenburg, and the Austrian Research Network ARiSE (Rigorous System Engineering).

1 0

2015-05: Inferring Lower Bounds for Runtime Complexity
by Thomas Ströder 14 Feb '15

14 Feb '15

The following technical report is available from http://aib.informatik.rwth-aachen.de: Inferring Lower Bounds for Runtime Complexity Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, and Thomas Ströder AIB 2015-05 We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.

1 0

2014-15: Synthesis of State Space Generators for Model Checking Microcontroller Code
by Thomas Ströder 08 Dec '14

08 Dec '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Synthesis of State Space Generators for Model Checking Microcontroller Code Dominique Gückel AIB 2014-15 Creating software for embedded systems requires rigid quality measures. The reason for this is that errors in the software may have very expensive or even disastrous consequences. This gives rise to the use of formal methods for software verification, such as model checking, theorem proving, and static analysis. Many embedded systems rely on either application-specific circuits, reconfigurable logics, or microcontrollers. Manufacturers of microcontrollers typically offer a wide variety of devices based on the same core architecture, which are equipped differently and thus offer different functionality. Furthermore, some tool chains exist that allow developers not only to choose from such off-the-shelf devices, but to customize them for specific kinds of tasks. In some cases, this may go to the extent of actually designing new architectures. It is precisely this wide variety of available devices that complicates the use of automated verification. Tools need to be adapted to a new platform, or even recreated in case they should be implemented in a too hardware-dependent way. The topic this thesis deals with is the reduction of the necessary effort for adapting a verification tool to new microcontrollers. To this end, we designed a language for describing microcontrollers, SGDL, and a compiler for translating such descriptions into operative simulators and static analyzers. We based our work on [mc]square, which is a platform for model checking and static analysis of assembly code software. In order to counter the state explosion problem, it is also necessary to include abstractions in generated simulators. We illustrate, on a number of abstraction techniques, how they can be integrated into the approach and whether they can be generated either partly or entirely. A number of case studies concerning the implementation of simulators with our new language is presented. Additionally, we examine the effectiveness of the aforementioned abstractions that are integrated into the generated simulators, and compare the results to those obtained when using manually implemented simulators.

1 0