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

-2009-05: A New Intersection Model and Improved Algorithms for Tolerance Graphs
by Carsten Fuhs 24 Mar '09

24 Mar '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: A New Intersection Model and Improved Algorithms for Tolerance Graphs George B. Mertzios, Ignasi Sau, Shmuel Zaks AIB 2009-05 Tolerance graphs model interval relations in such a way that intervals can tolerate a certain degree of overlap without being in conflict. This class of graphs, which generalizes in a natural way both interval and permutation graphs, has attracted many research efforts since their introduction in~\cite{GoMo82}, as it finds many important applications in constraint-based temporal reasoning, resource allocation, and scheduling problems, among others. In this article we propose the first non-trivial intersection model for general tolerance graphs, given by three-dimensional parallelepipeds, which extends the widely known intersection model of parallelograms in the plane that characterizes the class of bounded tolerance graphs. Apart from being important on its own, this new representation also enables us to improve the time complexity of three problems on tolerance graphs. Namely, we present optimal $\mathcal{O}(n\log n)$ algorithms for computing a minimum coloring and a maximum clique, and an $\mathcal{O}(n^{2})$ algorithm for computing a maximum weight independent set in a tolerance graph with $n$ vertices, thus improving the best known running times $\mathcal{O}(n^{2})$ and $\mathcal{O}(n^{3})$ for these problems, respectively.

1 0

2009-03: Model-Based Construction of Embedded & Real-Time Software - A Methodology for Small Devices
by Carsten Fuhs 22 Feb '09

22 Feb '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Model-Based Construction of Embedded & Real-Time Software - A Methodology for Small Devices Alexander Nyßen AIB 2009-03 While model-based software engineering - due to its increased abstraction and its advantages in terms of traceability and analyzability - seems to be the adequate means to deal with the increased complexity of software that one faces today, it does not seem to have penetrated all domains yet, in particular not the one of small embedded & real-time systems. Seeing this problem caused by the fact that current model-based approaches do not pay sufficient attention to the rather special technical, organizational, and economical constraints in the respective domain, this work presents an approach that explicitly takes these constraints into account. MeDUSA, a model-based software construction method for small embedded & real-time systems, is a principal item of the presented solution. To face the strong technical constraints it was especially designed as an instance-driven method, not incorporating any object-oriented concepts, but forcing a class-based design that can be seamlessly transferred into a procedural implementation, which is still state-of-the-art in the regarded domain. To guarantee such a seamless transition MeDUSA was furthermore designed to be a software construction rather than a mere design method, explicitly also addressing the implementation activities, and especially the transition from detailed design into source code. Being organized around the use case concept, the method excels at being very systematic and - inter alia by facilitating a continuous real-time analysis - also at being especially aware about the stringent real- time constraints that have to be faced in the domain of embedded & real-time systems. ViPER, the supporting tool prototype, forms the second essential part of the solution. It offers generic support for MeDUSA's modeling activities by providing a graphical UML modeling environment, as well as special support for the specification and simulation of narrative, textual use case details. It furthermore demonstrates dedicated methodical support by embedding a hypertext documentation of MeDUSA's definition, by providing implementations of the MeDUSA UML profiles and model constraints, and by offering dedicated wizards to support the execution of certain MeDUSA tasks. Together with their underlying languages, the Unified Modeling Language as well as the ANSI-C programming language, MeDUSA and ViPER thus form an integrated methodology, which is founded on shared concepts and principles. Especially developed to address above quoted constraints, the methodology is applicable to a domain, which has pretty much been elided so far.

1 0

2008-17: Static Termination Analysis for Prolog using Term Rewriting and SAT Solving
by Carsten Fuhs 22 Dec '08

22 Dec '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Static Termination Analysis for Prolog using Term Rewriting and SAT Solving Peter Schneider-Kamp AIB 2008-17 The most fundamental decision problem in computer science is the halting problem, i.e., given a description of a program and an input, decide whether the program terminates after finitely many steps or runs forever on that input. While Turing showed this problem to be undecidable in eneral, developing static analysis techniques that can automatically prove termination for many pairs of programs and inputs is of great practical interest. This is true in particular for logic programming, as the inherent lack of direction in the computation virtually guarantees that any non-trivial program terminates only for certain classes of inputs. Thus, termination of logic programs is widely studied and significant advances have been made during the last decades. Nowadays, there are fully-automated tools that try to prove termination of a given logic program w.r.t. a given class of inputs. Nevertheless, there still remain many logic programs that cannot be handled by any current termination technique for logic programs that is amenable to automation. Another area where termination has been studied even more intensively is term rewriting. This basic computation principle underlies the evaluation mechanism of many programming languages. Significant advances towards powerful automatable termination techniques during the last decade have yielded a plethora of powerful tools for proving termination automatically. In this thesis, we show that techniques developed for proving termination of term rewriting can successfully be adapted and applied to analyze logic programs. The new techniques developed significantly extend the applicability and the power of automated termination analysis for logic programs. The work presented here ranges from adapting techniques to work directly on logic programs to transformations from logic programs to a specialized version of term rewriting. On the logic programming side we also present a new pre-processing approach to handle logic programs with cuts. On the term rewriting side we show how to search for certain popular classes of well-founded orders on terms more efficiently by encoding the search into satisfiability problems of propositional logic. The contributions developed in this thesis are implemented in tools for automated termination analysis -- mostly in our fully automated termination prover AProVE. The significance of our results is demonstrated by the fact that AProVE has reached the highest score both for term rewriting and logic programming at the annual international Termination Competitions in all years since 2004, where the leading automated tools try to analyze termination of programs from different areas of computer science.

1 0

2008-18: Empirical Evaluations of Safety-Critical Embedded Systems
by Peter Schneider-Kamp 06 Nov '08

06 Nov '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Empirical Evaluations of Safety-Critical Embedded Systems Falk Salewski AIB 2008-18 Embedded systems based on different types of hardware platforms are nowadays increasingly used in safety-critical applications. These different hardware platforms lead to fundamental differences in design, particularly regarding the corresponding software. In this work, potential influences of hardware platforms on safety properties were gathered and open issues were identified. The most relevant of these open issues were evaluated for popular embedded hardware platforms (microcontroller, CPLD/FPGA). In detail, the impacts of hardware platform selection on software diversity, encapsulation, reviewability, reusability and the development according to ISO26262 were chosen for investigation. Furthermore, the approach of software diversity was compared with a fault removal approach. The evaluation was realized in form of six experiments conducted for this work. During these evaluations, the following similarities and differences were observed for the considered hardware platforms. Despite the diversity between the hardware platforms, failures observed in the software versions, which were developed for these different platforms, contained high numbers of dependent (coincident) failures. Although failure dependency between two versions was reduced by the use of diverse hardware platforms, this effect was low. Most dependent failures were identified as implementation independent so that improvements of the software diversity by hardware diversity were limited. Thus, a comparison of software fault tolerance with a fault removal approach based on tests and reviews was conducted. As a result, different types of failures were mitigated by these alternative approaches. On the other hand, differences between microcontrollers and FPGAs were observed. First, certain advantages of FPGAs with respect to encapsulation and reuse of real-time functions could be demonstrated. Moreover, differences regarding the reviewability of software versions written for FPGAs and microcontrollers were observed. Finally, the development according to ISO26262 revealed only minor differences between the investigated hardware platforms but between the different safety concepts of device supervision and function supervision.

1 0

2008-07: The MeDUSA Reference Manual, Second Edition
by Peter Schneider-Kamp 14 Jul '08

14 Jul '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: The MeDUSA Reference Manual, Second Edition Alexander Nyßen, Horst Lichter AIB 2008-07 MeDUSA (Method for UML2-based Construction of Embedded & Real-Time Software) is a model-based software construction method targeting the domain of small embedded & real-time software. MeDUSA was developed by the Research Group Software Construction of the RWTH Aachen University in close cooperation with the German ABB Corporate Research Centre. It incorporates various practical experiences gained during the industrial development of embedded software in ABB Business Unit Instrumentation. Being Use Case-driven, MeDUSA systematically covers the software construction lifecycle phase from the early requirements up to implementation. Models are successively developed and employed throughout all activities. By enforcing a class-based rather than an object-oriented design, a smooth transition of the resulting design model towards an implementation in a procedural programming language is facilitated. This is essential, as procedural programming languages as the C language are still state-of-the-art in the domain of small embedded & real-time software.

1 0

2008-16: Comparing recent network simulators: A performance evaluation study
by Peter Schneider-Kamp 07 Jul '08

07 Jul '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Comparing recent network simulators: A performance evaluation study Hendrik vom Lehn, Elias Weingärtner and Klaus Wehrle AIB 2008-16 Ranging from the development of new protocols to validating analytical performance metrics, network simulation is the most prevalent methodology in the field of computer network research. While the well known ns-2 toolkit has established itself as the quasi standard for network simulation, the successors are on their way. In this paper, we first survey recent contributions in the field of network simulation tools as well as related aspects such as parallel network simulation. Moreover, we present preliminary results which compare the resource demands for ns-3, JiST, SimPy and OMNeT++ by implementing the identical simulation scenario in all these simulation tools.

1 0

2008-15: A New Algorithm for Finding Trees with Many Leaves
by Peter Schneider-Kamp 25 Jun '08

25 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: A New Algorithm for Finding Trees with Many Leaves Joachim Kneis, Alexander Langer, Peter Rossmanith AIB 2008-15 We present an algorithm that finds trees with at least k leaves in undirected and directed graphs. These problems are known as Maximum Leaf Spanning Tree for undirected graphs, and, respectively, Directed Maximum Leaf Out-Tree and Directed Maximum Leaf Spanning Out-Tree in the case of directed graphs. The run time of our algorithm is O(poly(|V|) + 4^k k^2) on undirected graphs, and O(4^k |V| |E|) on directed graphs. Currently, the fastest algorithms for these problems have run times of O(poly(n) + 6.75^k poly(k)) and 2^{O(k log k)} poly(n), respectively.

1 0

2008-14: Model Checking Software for Microcontrollers
by Peter Schneider-Kamp 18 Jun '08

18 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Model Checking Software for Microcontrollers Bastian Schlich AIB 2008-14 Software of microcontrollers is getting more and more complex. It is mandatory to extensively analyze their software as errors can lead to severe failures or cause high costs. Model checking is a formal method used to verify whether a system satisfies certain properties. This thesis describes a new approach for model checking software for microcontrollers. In this approach, assembly code is used for model checking instead of an intermediate representation such as C code. The development of [MC]SQUARE, which is a microcontroller assembly code model checker implementing this approach, is detailed. [mc]square has a modular architecture to cope with the hardware dependency of this approach. The single steps of the model checking process are divided into separate packages. The creation of the states is conducted by a specific simulator, which is the only hardware-dependent package. Within the simulator, the different microcontrollers are modeled accurately. This work describes the modeling of the ATMEL ATmega16 microcontroller and details implemented abstraction techniques, which are used to tackle the state-explosion problem. These abstraction techniques include lazy interrupt evaluation, lazy stack evaluation, delayed nondeterminism, dead variable reduction, and path reduction. Delayed nondeterminism introduces symbolic states, which represent a set of states, into [MC]SQUARE while still explicit model checking techniques are used. Thus, we successfully combined explicit and symbolic model checking techniques. A formal model of the simulator, which we developed to prove the correctness of abstraction techniques, is described. In this work, the formal model is used to show the correctness of delayed nondeterminism. To show the applicability of the approach, two case studies are described. In these case studies, we used programs of different sizes. All these programs were created by students in lab courses, during diploma theses, or in exercises without the intention to use them for model checking.

1 0

2008-13: Improving Context-Sensitive Dependency Pairs
by Peter Schneider-Kamp 16 Jun '08

16 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Improving Context-Sensitive Dependency Pairs Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutierrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann AIB 2008-13 Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context- sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a "DP framework" for CS-DPs which would allow to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context- sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

1 0

2008-12: Abstraction for stochastic systems by Erlang's method of stages
by Peter Schneider-Kamp 06 Jun '08

06 Jun '08

The following technical report is available from http://aib.informatik.rwth-aachen.de: Abstraction for stochastic systems by Erlang's method of stages Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf AIB 2008-12 This paper proposes a novel abstraction technique based on Erlang's method of stages for continuous-time Markov chains (CTMCs). As abstract models Erlang-k interval processes are proposed where state residence times are governed by Poisson processes and transition probabilities are specified by intervals. We provide a three-valued semantics of CSL (Continuous Stochastic Logic) for Erlang-k interval processes, and show that both affirmative and negative verification results are preserved by our abstraction. The feasibility of our technique is demonstrated by a quantitative analysis of an enzyme-catalyzed substrate conversion, a well-known case study from biochemistry.

1 0