Universität Stuttgart
Permanent URI for this communityhttps://elib.uni-stuttgart.de/handle/11682/1
Browse
Search Results
Item Open Access Reachability analysis of multithreaded software with asynchronous communication(2005) Bouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejcek, JanWe introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.Item Open Access Emulation von Rechnernetzen zur Leistungsanalyse von verteilten Anwendungen und Netzprotokollen(2005) Herrscher, Daniel J.; Rothermel, Kurt (Prof. Dr. rer. nat. Dr. h. c)Um die Leistung von verteilten Anwendungen und Netzprotokollen in Abhängigkeit von den Eigenschaften der verwendeten Rechnernetze zu analysieren, wird eine Testumgebung benötigt, die Netzeigenschaften zuverlässig nachbilden ("emulieren") kann. Eine solche Testumgebung wird Emulationssystem genannt. Bisher existierende Emulationssysteme sind aufgrund ihrer Architektur entweder nur für sehr kleine Szenarien geeignet, oder sie können nur unabhängige Netzverbindungen nachbilden, und schließen damit alle Netztechnologien mit gemeinsamen Medien aus. In dieser Arbeit werden zunächst verschiedene Architekturvarianten für die Realisierung eines Emulationssystems vorgestellt und bewertet. Für die Variante mit zentraler Steuerung und verteilten Emulationswerkzeugen wird dann detailliert die Funktionalität eines Emulationssystems mit seinen wesentlichen Komponenten beschrieben. Das in dieser Arbeit entwickelte Emulationsverfahren greift auf der logischen Ebene der Sicherungsschicht in den Kommunikationsstapel ein. Auf dieser Ebene werden die beiden Basiseffekte Rahmenverlust und Verzögerung durch verteilte Emulationswerkzeuge nachgebildet. Alle anderen Netzeigenschaften können auf diese Basiseffekte zurückgeführt werden. Um Netztechnologien mit gemeinsamen Medien durch verteilte Werkzeuge nachbilden zu können, wird zusätzlich das Konzept des virtuellen Trägersignals eingeführt. Hierbei werden die Eigenschaften eines Rundsendemediums nachgebildet, indem kooperative Emulationswerkzeuge Rundsendungen zur Signalisierung eines Trägersignals benutzen. Somit kann jedeWerkzeuginstanz lokal ein aktuelles Modell des emulierten gemeinsamen Mediums halten. Auf dieser Basis kann auch das Verhalten von Medienzugriffsprotokollen nachgebildet werden. Die Arbeit deckt auch die wesentlichen Realisierungsaspekte eines Emulationssytems ab. Mit ausführlichen Messungen wird gezeigt, dass das entwickelte System für die Nachbildung von Netzszenarien sehr gut geeignet ist, selbst wenn die nachzubildenden Parameter sich dynamisch ändern. Die entwickelten Werkzeuge sind in der Lage, Netzeigenschaften in einem weiten Parameterbereich realistisch nachzubilden. Mit diesem System steht nun eine ideale Testumgebung für Leistungsmessungen von verteilten Anwendungen und Netzprotokollen in Abhängigkeit von Netzeigenschaften zur Verfügung.Item Open Access The design and implementation of a presentation system for interactive 3D graphics applications(2005) Stegmaier, Simon; Klein, Thomas; Strengert, Magnus; Ertl, ThomasWe present the design and implementation of a stand-alone system for presenting interactive 3D graphics applications and arbitrary multimedia contents to a public audience. The description includes technical details regarding the construction of a sturdy case to accommodate touchscreen, PC, video projector, and sound equipment, and details involved in the design of the presentation software. The presented system was evaluated during a week-long exhibition with several hundreds of users.Item Open Access Reguläre Häufigkeitsberechnungen(2005) Austinat, Holger; Diekert, Volker (Prof. Dr.)Die vorliegende Arbeit beschäftigt sich mit Häufigkeitsberechnungen, einem rekursionstheoretischen Begriff, der in den 60er Jahren von Rose eingeführt wurde. Eine Funktion f ist berechenbar mit Frequenz m/n, wenn es einen Algorithmus gibt, der für je n verschiedene Eingaben n Ausgabewerte berechnet, von denen mindestens m mit den zugehörigen Funktionswerten von f übereinstimmen. Eine erste natürliche Fragestellung war: gibt es nicht-berechenbare Funktionen, die mit einer Frequenz nahe 1 berechnet werden können? Trakhtenbrot beantwortete diese Frage 1963 negativ, indem er zeigte, dass eine Funktion mit Frequenz echt größer als 1/2 bereits berechenbar im herkömmlichen Sinne ist. Andererseits gibt es überabzählbar viele Funktionen, die sich mit Frequenz 1/2 berechnen lassen. Also ist dieses Ergebnis optimal. Die Forschung auf diesem Gebiet intensivierte sich daraufhin: Wissenschaftler wie Dëgtev, Kinber und Trakhtenbrot selbst (in den 70er und 80er Jahren) und Beigel, Gasarch, Hinrichs, Kummer, Stephan, Tantau und Wechsung (ab den 90er Jahren) beschäftigten sich mit verschiedenen Aspekten von Häufigkeitsberechnungen und verwandten Berechenbarkeitsbegriffen. In der vorliegenden Arbeit beschäftigen wir uns vorwiegend mit regulären Häufigkeitsberechnungen, also solchen, die von endlichen Automaten vorgenommen werden können. Kinber untersuchte diesen Aspekt als erster im Jahre 1976 und behauptete, dass sich Trakhtenbrots Resultat auf endliche Automaten überträgt. Sein folgerte dies aus einem allgemeineren Resultats über separierbare Sprachen, das sich allerdings als falsch herausstellte (ein Gegenbeispiel wurde 2002 von Tantau angegeben). (Zwei disjunkte Sprachen A und B heißen separierbar, wenn ein Algorithmus alle Wörter aus A akzeptiert und alle Wörter aus B ablehnt). Die Frage, ob das Analogon von Trakhtenbrots Resultat für endliche Automaten gilt, stellte sich also von neuem. Diese Dissertation enthält folgende Ergebnisse. In Kapitel 2 geben wir zwei Beweise für Trakhtenbrots Resultat an. Zunächst präsentieren wir seinen Originalbeweis, um dann einen neuen kombinatorischen Beweis zu geben, der einen großen Vorteil besitzt: er erlaubt die Übertragung des Ergebnisses auf endliche Automaten. Zwei kleinere Resultate beschließen dieses Kapitel: der Nachweis, dass es überabzählbar viele nicht häufigkeitsberechenbare Sprachen gibt, und eine Darstellung des Zusammenhangs von Häufigkeitsberechnungen und sog. mulit-selektiven Mengen. In Kapitel 3 arbeiten wir den Fehler in Kinbers Beweis über separierbare Sprachen heraus und geben ein konkretes Gegenbeispiel an. Dann untersuchen wir die Separierbarkeit von sog. Pfad- und Anti-Pfadsprachen, die wie folgt definiert sind: sei alpha ein unendliches Wort über dem Alphabet { 0, 1 }; dann ist A(alpha) die Menge der endlichen Präfixe von alpha, und B(alpha) die Menge der Wörter von A(alpha), bei denen das letzte Bit negiert wurde. Wir zeigen, dass A(alpha) und B(alpha) genau dann separiert werden können, wenn die 1-Positionen von alpha berechnet werden können. Andererseits gibt es überabzählbar viele alpha, für die A(alpha) und B(alpha) mit Frequenz 1/2 berechnet werden können. Wenn (ab drei Eingaben) nur ein Fehler zugelassen ist, dann sind A(alpha) und B(alpha) bereits rekursiv. Dieses Ergebnis überträgt sich auch auf endliche Automaten. Zum Abschluss dieses Kapitels zeigen wir, dass sich Kinbers Vermutung (dass Trakhtenbrots Resultat auch für Sprachen gilt, die durch endliche Automaten separiert werden können) nicht retten lässt: für jede Konstante q < 1 gibt es Werte 1 <= m < n mit m/n > q und ein alpha derart, dass A(alpha) und B(alpha) durch endliche Automaten mit Frequenz m/n separiert werden können, jedoch nicht rekursiv separierbar sind. In Kapitel 4 untersuchen wir verschiedene Aspekte regulärer Häufigkeitsberechnungen. Wir zeigen zunächst, dass sich Trakhtenbrots Resultat auf endliche Automaten überträgt, indem wir den neuen Beweis aus Kapitel 2 nochmals genauer betrachten. Anschließend zeigen wir, dass aperiodische Automaten, die Häufigkeitsberechnungen durchführen, nur aperiodische reguläre Sprachen berechnen können (aperiodische Sprachen entsprechen sternfreien Sprachen). Dann beweisen wir ein sog. Iterationskriterium, das vergleichbar mit dem bekannten Pumping-Lemma für reguläre Sprachen ist und uns für viele konkrete Beispielsprachen den Nachweis erlaubt, dass diese nicht häufigkeitsberechenbar sind. Im letzten Teil untersuchen wir dann Abschlusseigenschaften der Klasse der regulär häufigkeitsberechenbaren Sprachen: wir zeigen, dass sie eine boolesche Algebra bilden, jedoch nicht unter Spiegelung abgeschlossen sind. Darüberhinaus ist die Vereinigung zweier Sprachen, die mit Frequenz 1/n erkennbar sind, in der Regel nicht 1/n-erkennbar. Wir beweisen eine untere Schranke, die sehr nah an der besten bekannten oberen Schranke liegt.Item Open Access Laws for rewriting queries containing division operators(2005) Rantzau, Ralf; Mangold, ChristophRelational division, also known as small divide, is a derived operator of the relational algebra that realizes a many-to-one set containment test, where a set is represented as a group of tuples: Small divide discovers which sets in a dividend relation contain all elements of the set stored in a divisor relation. The great divide operator extends small divide by realizing many-to-many set containment tests. It is also similar to the set containment join operator for schemas that are not in first normal form. Neither small nor great divide has been implemented in commercial relational database systems although the operators solve important problems and many efficient algorithms for them exist. We present algebraic laws that allow rewriting expressions containing small or great divide, illustrate their importance for query optimization, and discuss the use of great divide for frequent itemset discovery, an important data mining primitive. A recent theoretic result shows that small divide must be implemented by special purpose algorithms and not be simulated by pure relational algebra expressions to achieve efficiency. Consequently, an efficient implementation requires that the optimizer treats small divide as a first-class operator and possesses powerful algebraic laws for query rewriting.Item Open Access Standardisierte Auszeichnungssprachen der Computergraphik für interaktive Systeme(2005) Rotard, Martin; Ertl, Thomas (Prof. Dr.)Computergraphik wird in vielen Bereichen der anwendungsorientierten Informatik, von der optischen Gestaltung graphischer Benutzungsoberflächen bis zur Visualisierung wissenschaftlicher Zusammenhänge eingesetzt. Auszeichnungssprachen zur Beschreibung graphischer Information erweitern diese Einsatzmöglichkeiten um die Animation und die Interaktion mit den Inhalten. In dieser Arbeit werden neue Verfahren und Strategien entwickelt, die den Einsatz von standardisierten Auszeichnungssprachen der Computergraphik in den Bereichen Benutzungsoberflächen und Lehrmaterialien ermöglichen. Dabei liegt ein Schwerpunkt auf der Zugänglichkeit von graphischen Inhalten für blinde Menschen, insbesondere durch interaktive Exploration von taktilen Darstellungen. Diese Arbeit stellt Methoden für die Beschreibung von skalierbaren Interaktionselementen mit Auszeichnungssprachen vor, die an verschiedenste Anzeigegeräte angepasst werden können. Darauf aufbauend entstanden neue Konzepte für zoombare Benutzungsoberflächen zur variablen Größendarstellung von Interaktionselementen und deren Inhalten. Erstmals werden auch Methoden vorgestellt, um die Darstellung von Benutzungsoberflächen, die mit Auszeichnungssprachen beschrieben werden, auf andere Rechner zu übertragen. Der Einsatz von Graphiken, die auf Auszeichnungssprachen basieren, bietet bei deren Erstellung, Handhabung und Anwendung erhebliche Vorteile gegenüber herkömmlicher Rastergraphik. Diese Arbeit stellt neue Verfahren vor, um die Formatierungen von Graphiken in Lehrmodulen anzupassen. Entwickelt werden unter anderem Konzepte für die Generierung von Lehrmodulen, die eine flexible Wiederverwendung in verschiedenen Lernszenarien ermöglichen. Für blinde Menschen bilden textuelle Inhalte die Hauptinformationsquelle bei ihrer Arbeit mit Computersystemen. Die ganzheitliche Darstellung von textuellen und graphischen Inhalten ist für viele Anwendungen jedoch unabdingbar. Mit Graphik, die auf Auszeichnungssprachen basiert, können erstmals Verfahren für die taktile Repräsentation präsentiert werden, die eine ganzheitliche Erschließung der graphischen Inhalte ermöglichen. Dazu werden Methoden vorgestellt, die blinden Menschen den Zugang zu mathematischen Ausdrücken, zu 2D- und zu 3D-Graphiken gestatten. Dies wird an einem taktilen Web-Browser demonstriert, der den Zugang zu diesen unterschiedlichen Graphikarten integriert.Item Open Access Inverse monoids : decidability and complexity of algebraic questions(2005) Lohrey, Markus; Ondrusch, NicoleThis paper investigates the word problem for inverse monoids generated by a set A subject to relations of the form e=f, where e and f are both idempotents in the free inverse monoid generated by A. It is shown that for every fixed monoid of this form the word problem can be solved in polynomial time which solves an open problem of Margolis and Meakin. For the uniform word problem, where the presentation is part of the input, EXPTIME-completeness is shown. For the Cayley-graphs of these monoids, it is shown that the first-order theory with regular path predicates is decidable. Regular path predicates allow to state that there is a path from a node x to a node y that is labeled with a word from some regular language. As a corollary, the decidability of the generalized word problem is deduced. Finally, it is shown that the Cayley-graph of the free inverse monoid has an undecidable monadic second-order theory.Item Open Access Model checking hierarchical structures(2005) Lohrey, MarkusHierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input graphs are defined hierarchical. In this paper, the model-checking problem for first-order logic (FO), monadic second-order logic (MSO), and second-order logic (SO) on hierarchically defined input graphs is investigated. It is shown that in general these model-checking problems are exponentially harder than their non-hierarchical counterparts, where the input graphs are given explicitly. As a consequence, several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Based on classical results of Gaifman and Courcelle, two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented.Item Open Access One evaluation of model-based testing and its automation(2005) Pretschner, Alexander; Prenninger, Wolfgang; Wagner, Stefan; Kühnel, Christian; Baumgartner, Martin; Sostawa, Bernd; Zölch, Rüdiger; Stauner, ThomasModel-based testing relies on behavior models for the generation of model traces: input and expected output - test cases - for an implementation. We use the case study of an automotive network controller to assess different test suites in terms of error detection, model coverage, and implementation coverage. Some of these suites were generated automatically with and without models, purely at random, and with dedicated functional test selection criteria. Other suites were derived manually, with and without the model at hand. Both automatically and manually derived model-based test suites detected significantly more requirements errors than hand-crafted test suites that were directly derived from the requirements. The number of detected programming errors did not depend on the use of models. Automatically generated model-based test suites detected as many errors as hand-crafted model-based suites with the same number of tests. A sixfold increase in the number of model-based tests led to an 11% increase in detected errors.Item Open Access Realizing enterprise integration patterns in WebSphere(2005) Scheibler, Thorsten; Leymann, FrankOver the last few years, patterns became focus of many activities in both, software development and research. Because of the financial significance of enterprise application integration (EAI) technologies corresponding patterns in this area are especially important and, thus, found a lot of interest. Even a standard textbook has been well-established in this space ("Enterprise Integration Patterns"). People are asking for guidelines about how to use the patterns from this textbook in their environment. A Whitepaper of Hohpe provides a sample integration scenario together with guidelines of how to implement this integration scenario based on a subset of the patterns in the BizTalk Server 2004 environment. In this document, we use the same scenario and the same patterns as in this Whitepapper and show how to implement them in WebSphere.