Institut für Informatik
Filtern
Erscheinungsjahr
Dokumenttyp
- Ausgabe (Heft) zu einer Zeitschrift (38)
- Dissertation (33)
- Diplomarbeit (24)
- Studienarbeit (19)
- Bachelorarbeit (14)
- Masterarbeit (14)
- Bericht (1)
Schlagworte
- Routing (5)
- Bluetooth (4)
- Knowledge Compilation (4)
- Netzwerk (4)
- Semantic Web (4)
- Software Engineering (4)
- VNUML (4)
- E-KRHyper (3)
- Netzwerksimulation (3)
- RIP-MTI (3)
Institut
Ziel dieser Arbeit war es, den in [Rhe06] dargestellten operationalen Ansatz zur Modelltransformation mit Hilfe der am Institut für Softwaretechnik der Universität Koblenz-Landau vorhandenen Bibliotheken "JGraLab" und "GReQL" in Java zu implementieren. Die Implementierung sollte beweisen, dass der aufgezeigte Transformationsansatz in der Praxis umsetzbar ist. Dies wurde durch verschiedene Beispiele bewiesen. Die geplante Verwendung in weiteren Projekten des IST wird für die Zukunft zeigen, ob sich weitere Transformationen umsetzten lassen oder wo die Grenzen des Ansatzes sind. Des weiteren ist denkbar, die Transformationen nicht mehr in zwei Schritten (Schematransformation vor Graphtransformation), sondern beide Schritte auf einmal ablaufen zu lassen. Dieser Schritt setzt jedoch voraus, dass JGraLab dies ebenfalls unterstützt.
Die Arbeitsgruppe Echtzeitsysteme an der Universität Koblenz beschäftigt sich seit mehreren Jahren mit der Thematik autonomes und assistiertes Fahren. Eine große Herausforderung stellen in diesem Zusammenhang mehrgliedrige Fahrzeuge dar, deren Steuerung für den Fahrer während der Rückwärtsfahrt sehr anspruchsvoll ist. Um präzise Manöver zu ermöglichen, können elektronische Fahrerassistenzsysteme zum Einsatz kommen. Im Rahmen vorhergehender Arbeiten sind bereits einige Prototypen entstanden, von denen jedoch keiner eine geeignete Lösung für moderne, zweiachsige Anhänger darstellt. Im Rahmen dieser Arbeit wurde ein prototypisches Fahrerassistenzsystem entwickelt, wobei es noch weiterer Forschungs- und Entwicklungsarbeit bedarf, um das System straßentauglich zu machen.
Diese Arbeit behandelt verschiedene Ansätze zur Ermittlung einer Heuristik, welche zur Bestimmung einer optimalen Konfiguration des Theorembeweisers E-KRHyper eingesetzt werden soll. Es wird erläutert, wie der Beweiser durch eine angepasste Voreinstellung optimiert werden kann und die erarbeiteten Ansätze zur Ermittlung dieser Voreinstellung werden vorgestellt. Anhand der erzielten Ergebnisse werden die Ansätze anschließend bewertet und für eines der vorgestellten Verfahren wird außerdem eine Idee zur Implementierung vorgestellt.
Die Beschreibung des Verhaltens eines Multi-Agenten-Systems (MAS) ist eine fordernde Aufgabe, besonders dann, wenn es in sicherheitskritischen Umgebungen eingesetzt werden soll. Denn in solchen Umgebungen muss die Beschreibung besonders sorgfältig ausgeführt werden um Seiteneffekte zu vermeiden, die ungewünschte oder sogar zerstörerische Folgen haben könnten. Deshalb sind formale Methoden nützlich, die auf mathematischen Modellen des zu entwerfenden Systems basieren. Sie erlauben es nicht nur das System formal auf verschiedenen Abstraktionsebenen zu spezifizieren, sondern auch seine Konsistenz noch vor der Implementierung zu verifizieren. Das Ziel der formalen Spezifikation ist eine präzise und eindeutige Beschreibung des Verhaltens des Multi-Agenten-Systems, während die Verifikation darauf abzielt, geforderte Eigenschaften dieses Systems zu beweisen. Üblicherweise wird das Verhalten eines Agenten als diskrete Änderung seines Zustands im Bezug auf externe oder interne Aktionen aufgefasst. Jedes mal, wenn eine Aktion auftritt, ändert sich der Zustand des Agenten. Deshalb sind Zustandsübergangsdiagramme bzw. endliche Automaten ein naheliegender Ansatz das Verhalten zu modellieren. Ein weiterer Vorteil einer solchen Beschreibung ist, dass sie sich für das sogenannte Model Checking eignet. Dabei handelt es sich um eine automatische Analysetechnik, die bestimmt, ob das Modell des Systems spezifizierten Eigenschaften genügt. Allerdings muss in realistischen, physikalischen Umgebungen neben dem diskreten auch das kontinuierliche Verhalten des Multi-Agenten-Systems betrachtet werden. Dabei könnte es sich beispielsweise um die Schussbewegung eines Fußballspieler-Agenten, den Prozess des Löschens durch einen Feuerwehr-Agenten oder jedes andere Verhalten handeln, das auf zeitlichen physikalischen Gesetzen basiert. Die üblichen Zustandsübergangsdiagramme sind nicht ausreichend, um diese beiden Verhaltensarten zu kombinieren. Hybride Automaten stellen jedoch eine elegante Lösung dar. Im Wesentlichen erweitern sie die üblichen Zustandsübergangsdiagramme durch Methoden, die sich mit kontinuierlichen Aktionen befassen. Die Zustandsübergänge modellieren weiterhin die diskreten Verhaltenswechsel, während Differentialgleichungen verwendet werden um das kontinuierliche Verhalten zu beschreiben. Besonders geeignet erscheinen Hybride Automaten, weil ihre formale Semantik die Verifikation durch Model Checking erlaubt. Deshalb ist das Hauptziel dieser Arbeit, Hybride Automaten für die Modellierung und die Verifikation des Verhaltens von Multi-Agenten-Systemen einzusetzen. Jedoch bringt ihr Einsatz mehrere Probleme mit sich, die betrachtet werden sollten. Zu diesen Problemfeldern zählen Komplexität, Modularität und die Aussagestärke der Modelle. Diese Arbeit befasst sich mit diesen Problemen und liefert mögliche Lösungen.
This paper shows how multiagent systems can be modeled by a combination of UML statecharts and hybrid automata. This allows formal system specification on different levels of abstraction on the one hand, and expressing real-time system behavior with continuous variables on the other hand. It is not only shown how multi-robot systems can be modeled by a combination of hybrid automata and hierarchical state machines, but also how model checking techniques for hybrid automata can be applied. An enhanced synchronization concept is introduced that allows synchronization taking time and avoids state explosion to a certain extent.
Hyper tableaux with equality
(2007)
In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.
Im Rahmen dieser Arbeit wird ein Programm in Java entwickelt, mit dem man sich beliebige Netzwerke graphisch anzeigen lassen kann. Diese Netzwerke müssen im Vorfeld mit Hilfe eines Configuration-Files beschrieben werden und dürfen nur aus Layer-2-Switches und Hosts aufgebaut sein. Nach Ladung eines solchen Files ins Programm kann das Netzwerk dort visualisiert werden. Darauf kann man dann den Spanning-Tree-Algorithmus IEEE 802.1D laufen lassen. Das Programm bietet auch die Möglichkeit, verschiedene Attribute der Switches und ihrer Ports nach Belieben einzustellen. Neben dem reinen Algorithmus werden die Hosts sich gegenseitig auch noch Normdaten zuschicken, wodurch die einzelnen STA-Mac-Tabellen aufgebaut werden. Ein weiteres Ziel ist es, die Switches mittels Threads parallel und unabhängig voneinander arbeiten zu lassen. Dies hat zur Folge, dass die Switches auf kein globales Wissen zugreifen können. Es gibt keine übergeordnete Instanz, die alle Switches lenkt und steuert. Diese Realisierung kommt der echten Arbeitsweise eines Netzwerks näher, als wenn alle Switches immer sofort über alle Abläufe Bescheid wissen.
Improvements to the RMTI network routing daemon implementation and preparation of a public release
(2011)
Routing with Metric based Topology Investigation (RMTI) is an algorithm meant to extend distance-vector routing protocols. It is under research and development at the University of Koblenz-Landau since 1999 and currently implemented on top of the well-known Routing Information Protocol (RIP). Around midyear 2009, the latest implementation of RMTI included a lot of deprecated functionality. Because of this, the first goal of this thesis was the reduction of the codebase to a minimum. Beside a lot of reorganization and a general cleanup, this mainly involved the removal of some no longer needed modes as well as the separation of the formerly mandatory XTPeer test environment. During the second part, many test series were carried out in order to ensure the correctness of the latest RMTI implementation. A replacement for XTPeer was needed and several new ways of testing were explored. In conjunction with this thesis, the RMTI source code was finally released to the public under a free software license.
An der Universität Koblenz wurde mit dem RMTI (RIP with Metric based Topology Investigation) eine Erweiterung zu RIP entwickelt, die das Counting-to-Infinity Problem beheben soll. Eine lauffähige Implementierung des RMTI Algorithmus, auf Basis des RIP Daemons der Quagga Software Routing Suite, liegt vor. Openwrt ist ein, auf Linux basierendes, quelloffenes Betriebssystem für Router, wie z.B. den WRT54G der Firma Linksys. Die Möglichkeiten der Konfiguration der Router mit Openwrt gehen weit über die der original Firmware hinaus. So können die Router mit Software aus dem Linux-Bereich erweitert werden. Ziel dieser Studienarbeit ist die Installation des RMTI Daemons in Openwrt auf den Linksys WRT54G Routern der AG Rechnernetze. Anschließend sollen typische Netzwerksituationen aufgebaut und das Verhalten der Router untersucht werden.
Interactive video retrieval
(2006)
The goal of this thesis is to develop a video retrieval system that supports relevance feedback. One research approach of the thesis is to find out if a combination of implicit and explicit relevance feedback returns better retrieval results than a system using explicit feedback only. Another approach is to identify a model to weight existing feature categories. For this purpose, a state-of-the-art analysis is presented and two systems implemented, which run under the conditions of the international TRECVID workshop. It will be a basis system for further research approaches in the field of interactive video retrieval. Amongst others, it shall participate in the 2006 search task of the mentioned workshop.