KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Fri, 15 Jun 2012 13:19:56 +0200Fri, 15 Jun 2012 13:19:56 +0200Deklarative Spezifikation von Datentransformationen
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/3175
Deklarative Spezifikation von Datentransformationen.Mathias Weberreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/3175Fri, 15 Jun 2012 13:19:56 +0200Statistical RNA Secondary Structure Sampling Based on a Length-Dependent SCFG Model
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/3152
One of the fundamental problems in computational structural biology is the prediction of RNA secondary structures from a single sequence. To solve this problem, mainly two different approaches have been used over the past decades: the free energy minimization (MFE) approach which is still considered the most popular and successful method and the competing stochastic context-free grammar (SCFG) approach. While the accuracy of the MFE based algorithms is limited by the quality of underlying thermodynamic models, the SCFG method abstracts from free energies and instead tries to learn about the structural behavior of the molecules by training the grammars on known real RNA structures, making it highly dependent on the availability of a rich high quality training set. However, due to the respective problems associated with both methods, new statistics based approaches towards RNA structure prediction have become increasingly appreciated. For instance, over the last years, several statistical sampling methods and clustering techniques have been invented that are based on the computation of partition functions (PFs) and base pair probabilities according to thermodynamic models. A corresponding SCFG based statistical sampling algorithm for RNA secondary structures has been studied just recently. Notably, this probabilistic method is capable of producing accurate (prediction) results, where its worst-case time and space requirements are equal to those of common RNA folding algorithms for single sequences.
The aim of this work is to present a comprehensive study on how enriching the underlying SCFG by additional information on the lengths of generated substructures (i.e. by incorporating length-dependencies into the SCFG based sampling algorithm, which is actually possible without significant losses in performance) affects the reliability of the induced RNA model and the accuracy of sampled secondary structures. As we will see, significant differences with respect to the overall quality of generated sample sets and the resulting predictive accuracy are typically implied. In principle, when considering the more specialized length-dependent SCFG model as basis for statistical sampling, a higher accuracy of predicted foldings can be reached at the price of a lower diversity of generated candidate structures (compared to the more general traditional SCFG variant or sampling based on PFs that rely on free energies).Markus E. Nebel; Anika Scheidreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/3152Mon, 21 May 2012 19:19:25 +0200Translating SHIM to Guarded Actions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2881
SHIM is a concurrent deterministic programming language for embedded systems built on rendezvous communication. It abstracts away many details to give the developer a high-level view that includes virtual shared variables, threads as orthogonal statements, and deterministic concurrent exceptions.
In this paper, we present a new way to compile a SHIM-like language into a set of asynchronous guarded actions, a well-established intermediate representation for concurrent systems. By doing so, we build a bridge to many other tools, including hardware synthesis and formal verification. We present our translation in detail, illustrate it through examples, and show how the result can be used by various other tools.Jens Brandt; Klaus Schneiderreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2881Tue, 14 Feb 2012 02:51:56 +0000Separate Translation of Synchronous Programs to Guarded Actions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2296
This report gives an overview of the separate translation of synchronous imperative programs to synchronous guarded actions. In particular, we consider problems to be solved for separate compilation that stem from preemption statements and local variable declarations. We explain how we solved these problems and sketch our solutions implemented in the our Averest framework to implement a compiler that allows a separate compilation of imperative synchronous programs with local variables and unrestricted preemption statements. The focus of the report is the big picture of our entire design flow.Jens Brandt; Klaus Schneiderreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2296Fri, 25 Mar 2011 14:43:06 +0100Non Uniform Generation of Combinatorial Objects
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2220
In this article we present a method to generate random objects from a large variety of combinatorial classes according to a given distribution. Given a description of the combinatorial class and a set of sample data our method will provide an algorithm that generates objects of size n in worst-case runtime O(n^2) (O(n log(n)) can be achieved at the cost of a higher average-case runtime), with the generated objects following a distribution that closely matches the distribution of the sample data.Frank Weinberg; Markus Nebelreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2220Wed, 21 Jul 2010 16:59:22 +0200First DASMOD Workshop on Verification of Adaptive Systems (VerAS)
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2101
This technical report contains the preliminary versions of the regular papers presented at the first workshop on Verification of Adaptive Systems (VerAS) that has been held in Kaiserslautern, Germany, on September 14th, 2007 as part of the 20th International Conference on Theorem Proving in Higher Order Logics. The final versions will be published with Elsevier's Electronic Notes on Theoretical Computer Science (ENTCS). VerAS is the first workshop that aims at considering adaptation as a cross-cutting system aspect that needs to be explicitly addressed in system design and verification. The program committee called for original submissions on formal modeling, specification, verification, and implementation of adaptive systems. There were six submissions from different countries of Europe. Each submission has been reviewed by three programme committee members. Finally, the programme committee decided to accept three of the six submissions. Besides the presentations of the regular papers, the workshop's programme included a tutorial on the `Compositional Verification of Self-Optimizing Mechatronic Systems' held by Holger Giese (University of Paderborn, Germany) as well as three presentations of DASMOD projects on the verification of adaptive systems.Arnd Poetzsch-Heffter; Klaus Schneiderconferenceobjecthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2101Wed, 03 Jun 2009 14:55:10 +0200Theorem Proving in Higher Order Logics - Emerging Trends
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2100
This technical report is the Emerging Trends proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), which was held during 10-13 September in Kaiserslautern, Germany. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and veriﬁcation.Klaus Schneider; Jens Brandtconferenceobjecthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2100Wed, 03 Jun 2009 14:54:52 +0200Evaluation eines Verschmelzungsalgorithmus für Lösungen des Handlungsreisendenproblems
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2082
Das Handlungsreisendenproblem ist eines der bekanntesten NP-vollständigen kombinatorischen Optimierungsprobleme. Algorithmen mit unterschiedlichen Konzepten und Strategien wurden entwickelt, die sich in Lösungsqualität und Laufzeit unterscheiden. Ein vergleichsweise neuer Ansatz stellt jedoch das Kombinieren vorhandener Lösungen dar. Hier werden die Kantenmengen gegebener Handlungsreisendertouren als Ausgangsbasis für weitere Optimierungen verwendet. Erste Veröffentlichungen zu diesem Gebiet stellen bereits vielversprechende Ergebnisse vor, die nachfolgend vertieft evaluiert werden.Thomas Fischerreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2082Wed, 29 Apr 2009 12:21:13 +0200Embedding a Chained Lin-Kernighan
Algorithm into a Distributed Algorithm
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2081
The Chained Lin-Kernighan algorithm (CLK) is one of the best heuristics to solve Traveling Salesman Problems (TSP). In this paper a distributed algorithm is proposed, were nodes in a network locally optimize TSP instances by using the CLK algorithm. Within an Evolutionary Algorithm (EA) network-based framework the resulting tours are modified and exchanged with neighboring nodes. We show that the distributed variant finds better tours compared to the original CLK given the same amount of computation time. For instance fl3795, the original CLK got stuck in local optima in each of 10 runs, whereas the distributed algorithm found optimal tours in each run requiring less than 10 CPU minutes per node on average in an 8 node setup. For instance sw24978, the distributed algorithm had an average solution quality of 0.050% above the optimum, compared to CLK's average solution of 0.119% above the optimum given the same total CPU time (104 seconds). Considering the best tours of both variants for this instance, the distributed algorithm is 0.033% above the optimum and the CLK algorithm 0.099%.Thomas Fischer; Peter Merzreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2081Wed, 29 Apr 2009 12:21:00 +0200ChordNet: Protocol Specification and Analysis
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2068
This work specifies and analyzes the ChordNet protocol. ChordNet is able to connect huge numbers of nodes in an efficient peer-to-peer network.Dennis Schwerdel; Matthias Priebe; Paul Müller; Peter Merzreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/2068Thu, 26 Feb 2009 12:15:44 +0100On the Expected Free Energy of RNA Molecules
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1946
This article focuses on the analytical analysis of the free energy in a realistic model for RNA secondary structures. In fact, the free energy in a stochastic model derived from a database of small and large subunit ribosomal RNA (SSU and LSU rRNA) data is studied. A common thermody-namic model for computing the free energy of a given RNA secondary structure, as well as stochastic context-free grammars and generating functions are used to derive the desired results. These results include asymptotics for the expected free energy and for the corresponding variance of a random RNA secondary structure. The quality of our model is judged by comparing the derived results to the used database of SSU and LSU rRNA data. At the end of this article, it is discussed how our results could be used to help on identifying good predictions of RNA secondary structure.Anika Scheid; Markus Nebelreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1946Mon, 07 Apr 2008 17:07:38 +0200On Abstract Shapes of RNA
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1945
As any RNA sequence can be folded in many different ways, there are lots of different possible secondary structures for a given sequence. Most computational prediction methods based on free energy minimization compute a number of suboptimal foldings and we have to identify the native structures among all these possible secondary structures. For this reason, much effort has been made to develop approaches for identifying good predictions of RNA secondary structure. Using the abstract shapes approach as introduced by Giegerich et al., each class of similar secondary structures is represented by one shape and the native structures can be found among the top shape representatives. In this article, we derive some interesting results answering enumeration problems for abstract shapes and secondary structures of RNA. We start by computing symptotical representations for the number of shape representations of length n. Our main goal is to find out how much the search space can be reduced by using the concept of abstract shapes. To reach this goal, we analyze the number of secondary structures and shapes compatible with an RNA sequence of length n under the assumption that base pairing is allowed between arbitrary pairs of bases analytically and compare their exponential growths. Additionally, we analyze the number of secondary structures compatible with an RNA sequence of length n under the assumptions that base pairing is allowed only between certain pairs of bases and that the structures meet some appropriate conditions. The exponential growth factors of the resulting asymptotics are compared to the corresponding experimentally obtained value as given by Giegerich et al.Anika Scheid; Markus Nebelreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1945Mon, 07 Apr 2008 15:24:23 +0200On Certifying Code Generation
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1913
Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.Jan Olaf Blechreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1913Mon, 03 Dec 2007 12:01:44 +0100On Translation Validation for System Abstractions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1893
Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of embedded adaptive systems. This paper is an extended version a previously published work.Jan Olaf Blech; Ina Schaefer; Arnd Poetzsch-Heffterreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1893Fri, 31 Aug 2007 22:35:38 +0200On the Complexity of the Uncapacitated Single Allocation p-Hub Median Problem with Equal Weights
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1885
The Super-Peer Selection Problem is an optimization problem in network topology construction. It may be cast as a special case of a Hub Location Problem, more exactly an Uncapacitated Single Allocation p-Hub Median Problem with equal weights. We show that this problem is still NP-hard by reduction from Max Clique.Steffen Wolfreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1885Tue, 24 Jul 2007 10:54:28 +0200Mapping of formal Network Quality-of-Service Requirements
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1853
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Since QoS functionalities are integrated across layers and hence QoS specifications exist on different system layers, a QoS mapping technique is needed to translate the specifications into each other. In this paper, we formalize the relationship between layers. Based on a comprehensive and holistic formalization of network QoS requirements, we define two kinds of QoS mappings. QoS domain mappings associate QoS domains of two abstraction levels. QoS scalability mappings associate utility and cost functions of two abstraction levels. We illustrate our approach by examples from the case study Wireless Video Transmission.Webel Christian; Gotzhein Reinhard; Schneider Danielreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1853Sun, 15 Apr 2007 00:41:54 +0200Formalization of Network Quality-of-Service Requirements
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1852
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Existing approaches to the specification of network QoS requirements are mainly focused on specific domains or individual system layers. In this paper, we present a holistic, comprehensive formalization of network QoS requirements, across layers. QoS requirements are specified on each layer by defining QoS domain, consisting of QoS performance, reliability, and guarantee, and QoS scalability, with utility and cost functions. Furthermore, we derive preorders on multi-dimensional QoS domains, and present criteria to reduce these domains, leading to a manageable subset of QoS values that is sufficient for system design and implementation. We illustrate our approach by examples from the case study Wireless Video Transmission.Webel Christian; Gotzhein Reinhard; Schneider Danielreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1852Sun, 15 Apr 2007 00:41:42 +0200Certifying Compilers based on Formal Translation Contracts
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1814
A translation contract is a binary predicate corrTransl(S,T) for source programs S and target programs T. It precisely specifies when T is considered to be a correct translation of S. A certifying compiler generates --in addittion to the target T-- a proof for corrTransl(S,T). Certifying compilers are important for the development of safety critical systems to establish the behavioral equivalence of high-level programs with their compiled assembler code. In this paper, we report on a certifying compiler, its proof techniques, and the underlying formal framework developed within the proof assistent Isabelle/HOL. The compiler uses a tiny C-like language as input, has an optimization phase, and generates MIPS code. The underlying translation contract is based on a trace semantics. We investigate design alternatives and discuss our experiences.Marek Jerzy Gawkowski; Jan Olaf Blech; Arnd Poetzsch-Heffterpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1814Sat, 25 Nov 2006 01:52:44 +0100Phishing in the Wireless: Implementation and Analysis
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1812
Web-based authentication is a popular mechanism implemented by Wireless Internet Service Providers (WISPs) because it allows a simple registration and authentication of customers, while avoiding the high resource requirements of the new IEEE 802.11i security standard and the backward compatibility issues of legacy devices. In this work we demonstrate two different and novel attacks against web-based authentication. One attack exploits operational anomalies of low- and middle-priced devices in order to hijack wireless clients, while the other exploits an already known vulnerability within wired-networks, which in dynamic wireless environments turns out to be even harder to detect and protect against.Ivan Martinovic; Frank A. Zdarsky; Adam Bachorek; Christian Jung; Jens B. Schmittreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1812Wed, 22 Nov 2006 13:41:36 +0100SDL Profiles - Definition and Formal Extraction
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1807
Over a period of 30 years, ITU-T’s Specification and Description Language (SDL) has matured to a sophisticated formal modelling language for distributed systems and communication protocols. The language definition of SDL-2000, the latest version of SDL, is complex and difficult to maintain. Full tool support for SDL is costly to implement. Therefore, only subsets of SDL are currently supported by tools. These SDL subsets - called SDL profiles - already cover a wide range of systems, and are often suffcient in practice. In this report, we present our approach for extracting the formal semantics for SDL profiles from the complete SDL semantics. We then formalise the approach, present our SDL-profile tool, and report on our experiences.Rüdiger Grammes; Reinhard Gotzheinreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1807Tue, 21 Nov 2006 12:53:38 +0100Adding Position Structures to Katja
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1794
This document introduces the extension of Katja to support position structures and explains the subtleties of their application as well as the design decisions made and problems solved with respect to their implementation. The Katja system was first introduced by Jan Schäfer in the context of his project work and is based on the MAX system developed by Arnd Poetzsch-Heffter.Patrick Michelreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1794Tue, 31 Oct 2006 02:29:18 +0100Redesign and Enhancement of the Katja System
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1795
Katja is a tool generating order-sorted recursive data types as well as position types for Java, from specifications using an enhanced ML like notation. Katja’s main features are its conciseness of specifications, the rich interface provided by the generated code and the Java atypical immutability of types. After several stages of extending and maintaining the Katja project, it became apparent many changes had to be done. The original design of Katja wasn’t prepared for the introduction of several backends, the introduction of position sorts and constant feature enhancements and bug fixes. By supplying this report Katja reaches release status for the first time.Patrick Michelreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1795Tue, 31 Oct 2006 02:29:05 +0100Formalisation of the UML Profile for SDL - A Case Study
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1792
With the UML 2.0 standard, the Unified Modeling Language took a big step towards SDL, incorporating many features of the language. SDL is a mature and complete language with formal semantics. The Z.109 standard defines a UML Profile for SDL, mapping UML constructs to corresponding counterparts in SDL, giving them a precise semantics. In this report, we present a case study for the formalisation of the Z.109 standard. The formal definition makes the mapping precise and can be used to derive tool support.Rüdiger Grammesreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1792Fri, 27 Oct 2006 14:00:46 +0200Simple Loose Ownership Domains
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1724
Ownership Domains generalize ownership types. They support programming patterns like iterators that are not possible with ordinary ownership types. However, they are still too restrictive for cases in which an object X wants to access the public domains of an arbitrary number of other objects, which often happens in observer scenarios. To overcome this restriction, we developed so-called loose domains which abstract over several precise domains. That is, similar to the relation between supertypes and subtypes we have a relation between loose and precise domains. In addition, we simplified ownership domains by reducing the number of domains per object to two and hard-wiring the access permissions between domains. We formalized the resulting type system for an OO core language and proved type soundness and a fundamental accessibility property.Jan Schäfer; Arnd Poetzsch-Heffterreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1724Sat, 01 Apr 2006 13:01:09 +0200Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1681
There is a well known relationship between alternating automata on finite words and symbolically represented nondeterministic automata on finite words. This relationship is of practical relevance because it allows to combine the advantages of alternating and symbolically represented nondeterministic automata on finite words. However, for infinite words the situation is unclear. Therefore, this work investigates the relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Thereby, we identify classes of alternating omega-automata that are as expressive as safety, liveness and deterministic prefix automata, respectively. Moreover, some very simple symbolic nondeterminisation procedures are developed for the classes corresponding to safety and liveness properties.Thomas Tuerk; Klaus Schneiderreporthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/1681Thu, 17 Nov 2005 10:46:49 +0100