Institut für Informatik
Filtern
Erscheinungsjahr
- 2010 (18) (entfernen)
Dokumenttyp
- Diplomarbeit (6)
- Ausgabe (Heft) zu einer Zeitschrift (6)
- Studienarbeit (4)
- Bachelorarbeit (1)
- Dissertation (1)
Schlagworte
- Netzwerk (2)
- Routing (2)
- hybrid automata (2)
- API (1)
- Algorithm Engineering (1)
- Authentisierung (1)
- Automatisches Beweisverfahren (1)
- Computational logic (1)
- Context-aware processes (1)
- Controlling (1)
- Description Logics (1)
- Dijkstras Algorithmus (1)
- Distributed process execution (1)
- E-KRHyper (1)
- GPS (1)
- Heuristiken (1)
- JML (1)
- Java Modeling Language (1)
- Java. Programmiersprache (1)
- Klausellogik (1)
- Knowledge Compilation (1)
- Konvergenz (1)
- Mikrocontroller (1)
- Monitoring (1)
- Multiagentensysteme (1)
- Network (1)
- Netzwerk Protokollen (1)
- Neuronales Netz (1)
- Oracle Generation (1)
- Oraklegenerierung (1)
- Personal Key Infrastruktur (1)
- Petri net (1)
- Probability propagation nets (1)
- Process tracing (1)
- Projekt iCity (1)
- Protocol (1)
- Prädikatenlogik (1)
- RIP (1)
- RMTI (1)
- Rechnernetz (1)
- Software Engineering (1)
- Softwaretest (1)
- Softwaretesting (1)
- Spannender Baum (1)
- Spanning Tree (1)
- Specification (1)
- Spezifikation (1)
- Statistische Analyse (1)
- Tableau <Logik> (1)
- Test Generation (1)
- Testgenerierung (1)
- VNUML (1)
- Wireshark (1)
- XTPeer (1)
- Zertifikat (1)
- andLinux (1)
- andLinux. (1)
- backpropagation (1)
- bias (1)
- constraint logic programming (1)
- convergence analysis (1)
- ediv (1)
- hybride Automaten (1)
- iCity project (1)
- multi-agent systems (1)
- multiagent systems (1)
- networks (1)
- neural (1)
- privacy protection (1)
- public key infrastructure (1)
- recurrent (1)
- rip (1)
- rmti (1)
- vnuml (1)
- xtpeer (1)
Institut
- Institut für Informatik (18)
- Fachbereich 4 (6)
Die vorliegende Arbeit stellt eine Methode für die korpusbasierte Analyse der Verwendung von Softwarebibliotheken in Java-Programmen vor. Die meisten größeren Softwareprojekte verwenden Softwarebibliotheken, die als Schnittstelle für den Programmierer sogenannte APIs (application programming interfaces) bereitstellen. Um den Umstieg von einer solchen API auf eine andere zu unterstützen, strebt man Werkzeuge zur automatisierten API-Migration an. Zur Entwicklung solcher Werkzeuge fehlen allerdings noch Basisdaten. Statistiken und Beobachtungen zur Verwendung von APIs in der Praxis wurden bisher nur mit sehr kleinen Korpora von Projekten und APIs durchgeführt. Wir stellen in dieser Arbeit daher eine Analysemethode vor, die für Messungen an großen Korpora geeignet ist. Hierzu erzeugen wir zunächst einen Korpus von auf SourceForge gehosteten Open-Source-Projekten sowie einen Korpus von Softwarebibliotheken. In der Folge werden alle Projekte des Korpus compiliert, wobei ein Compiler-Plugin für den javac detaillierte Informationen über jede einzelne Methode liefert, die der Compiler erstellt. Diese Informationen werden in einer Datenbank gespeichert und analysiert.
Conventional security infrastructures in the Internet cannot be directly adopted to ambient systems, especially if based on short-range communication channels: Personal, mobile devices are used and the participants are present during communication, so privacy protection is a crucial issue. As ambient systems cannot rely on an uninterrupted connection to a Trust Center, certiffed data has to be veriffed locally. Security techniques have to be adjusted to the special environment. This paper introduces a public key infrastructure (PKI) to provide secure communication channels with respect to privacy, confidentiality, data integrity, non-repudiability, and user or device authentication. It supports three certiffcate levels with a different balance between authenticity and anonymity. This PKI is currently under implementation as part of the iCity project.
In einer Welt, die immer mehr durch den Einsatz von Technik geprägt wird, gewinnen Systeme, welche eigenständig Aufgaben in einem vorgegebenen Kontext übernehmen können, mehr und mehr an Bedeutung. Solche Systeme werden als autonome Systeme bezeichnet, die ein eigenständiges Verhalten und Interaktionen mit ihrer Umwelt und anderen Systemen beinhalten. Zu diesen Systemen zählen auch autonome mobile Roboter. Sie sind sozusagen intelligente Fahrzeuge, die ihnen übertragene Aufgaben ohne menschliche Unterstützung durchführen können. Um ihre Umwelt wahrzunehmen, mit ihr interagieren und in ihr navigieren zu können benötigen diese Systeme verschiedene Arten von Sensoren. Somit ist die Robotikforschung stark interdisziplinär. Diese Arbeit befasst sich ausschliesslich mit dem Bereich der Navigation, insbesondere mit der Positionsbestimmung, welche für eine gute Navigation die Grundlage bildet. Ein heutzutage häufig benutztes, weltweit verfügbares System zur Positionsbestimmung ist GPS. Ziel dieser Arbeit ist der Anschluss eines GPS-Moduls an einen Mikrocontroller und der Versuch die Positionsgenauigkeit lokal zu präzisieren, um so einem autonomen System die Möglichkeit zur eröffnen, Aufgaben, die eine höhere Genauigkeit erfordern, zu bewerkstelligen.
RMTI (RIP with Metric based Topology Investigation) wurde in der AG Rechnernetze an der Universität Koblenz-Landau entwickelt. RMTI stellt eine Erweiterung zum RIP (Routing Information Protocol) dar, die das Konvergenzverhalten bei Netzwerkveränderungen, insb. bei Routingschleifen, verbessern soll. Dies geschieht durch Erkennen von Routingschleifen und Reduzieren des Count-to-infinity Problems. Um dieses gewünschte Verhalten nachweisen zu können, bedarf eine reichhaltige Evaluierung des RMTI- Algorithmus. Hierzu wurde in der gleichen Arbeitsgruppe die Client-/Server-Applikation XTPeer entwickelt. In Kombination mit anderen Software wie VNUML und Quagga Routing Suite lässt sich per XT-Peer der Algorithmus evaluieren. Die Applikation XTPeer generiert durch die Simulationen Daten. Diese können in Form von XML konforme SDF-Dateien exportiert werden. Diese können ohne weitere Auswertungen wieder in die XTPeer Applikation importiert werden. Die Evaluierung der Simulationen findet automatisiert nur an der aktuellen Simulation statt. Evaluierung über mehrere Simulationen muss der Benutzer manuell berechnen. Um diese Evaluierungsarbeiten für den Benutzer zu vereinfachen, verfolgt die vorliegende Diplomarbeit daher das Ziel, die XTPeer Applikation mit einem Auswertungsmodul zu erweitern. Die Auswertungen soll sich über alle gespeicherten Simulationsdaten und nicht wie bisher nur über die aktuell laufende Simulation erstrecken. Dies ermöglicht bessere statistisch verwertbare Aussagen. Zusätzlich können diese Auswertungsergebnisse grafisch unterstrichen werden.
This thesis introduces fnnlib, a C++ library for recurrent neural network simulations that I developed between October 2009 and March 2010 at Osaka University's Graduate School of Engineering. After covering the theory behind recurrent neural networks, backpropagation through time, recurrent neural networks with parametric bias, continuous-time recurrent neural networks, and echo state networks, the design of the library is explained. All of the classes as well as their interrelationships are presented along with reasons as to why certain design decisions were made. Towards the end of the thesis, a small practical example is shown. Also, fnnlib is compared to other neural network libraries.
This minor thesis shows a way to optimise a generated oracle to achieve shorter runtimes. Shorter runtimes of test cases allows the execution of more test cases in the same time. The execution of more test cases leads to a higher confidence in the software-quality. Oracles can be derived from specifications. However specifications are used for different purposes and therefore are not necessarily executable. Even if the are executable it might be with only a high runtime. Those two facts come mostly from the use of quantifiers in the logic. If the quantifier-range is not bounded, respectively if the bounds are outside the target language-datatype-limits, the specification is too expressive to be exported into a program. Even if the bounds inside the used datatype-limits, the quantification is represented as a loop which leads to a runtime blowup, especially if quantifiers are nested. This work explains four different possibilities to reduce the execution time of the oracle by manipulating the quantified formular whereas this approach is only applicable if the quantified variables are of type Integer.
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.
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.