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
- Institut für Informatik (143) (entfernen)
Der an der Universität Koblenz-Landau entwickelte RIP-MTI-Algorithmus stellt eine Modifikation des Routingalgorithmus RIP dar, die es dem RIP-Algorithmus ermöglichen soll, die Häufigkeit des Auftretens des Counting-to-infinity-Problems (CTI) zu reduzieren. Um die Korrektheit und Zuverlässigkeit dieses Algorithmus nachweisen, aber auch Schwächen aufdecken zu können, bedarf es der Möglichkeit, das Verhalten des Algorithmus zu testen. Ziel der Arbeit ist die Nutzbarmachung der von unter VNUML laufenden RIP-Routern dezentral verwalteten Routing-Informationen, um die Entstehung von CTIs zentral protokollieren und analysieren zu können. Zu diesem Zweck wird eine Software entwickelt, die Informationen zur Netzkonfiguration, zu Erreichbarkeiten und Update-Aufkommen sammelt, verwaltet und analysiert. So können neben den bereits bekannten problematischen Netztopologien weitere für die einzelnen RIP-Ausprägungen problematische Topologien ermittelt werden.
E-Learning Anwendungen sind heutzutage im Trend. Jedoch nicht nur aus diesem Grund sind sie vom großen Interesse. Im Vordergrund steht ihr didaktisches Konzept. Heutzutage ist es technisch möglich, die Teilnehmer interaktiv in einen
E- Learning Kurs einzubinden. Die Lernschritte können durch die Anwendung kontrolliert werden. Im Gegensatz zu einer Vorlesung, kann die Theorie direkt mit der Praxis verknüpft werden. Das Ziel der Arbeit ist die Erstellung eines Konzeptes und die Entwicklung eines Prototypen einer interaktiven Entwicklungsumgebung von Java für Programmieranfänger. In dieser Arbeit wurden aktuelle E-Learning Plattformen zu Java analysiert. Aus den gewonnen Erkenntnissen wurde ein Konzept für eine E-Learningplattform entwickelt. Dieses Konzept wurde erfolgreich als Prototyp implementiert. Für die Implementation wurden bewährte Technologien, wie das Django-Framework und das Javascript-Framework Vue.js eingesetzt. Der Kurs wurde von neun Teilnehmern getestet. Zusätzlich wurde eine Umfrage zu der Kursanwendung durchgeführt. Das Testergebnis bestätigt, dass die Teilnehmer den Kurs bestanden haben.
Der RIPMTI-Algorithmus wurde entwickelt um die Schleifenerkennung in Rechnernetzen zu verbessern. Das Count-To-Infinity-Problem (kurz: CTI) führt dazu, dass ein Netzwerk nur sehr langsam in einen konvergenten Zustand gelangt. Der Hopcount-Wert 16, der als künstliche Beschränkung des CTI eingeführt wurde, beschränkt leider auch die maximale Topologietiefe eines Netzwerkes. Diese Arbeit soll zeigen wie sich eine schrittweise Erhöhung des Hopcount-Wertes und darüber hinaus die Änderung der Updatezeiten jedes Routers auf die Konvergenzzeiten unterschiedlicher Netzwerk-Szenarios auswirkt.
Die vorliegende Dissertation untersucht die Entstehung von Dialekten innerhalb des in dieser Arbeit entworfenen Modells einer Multi-Agenten-Simulation, basierend auf neuronalen Netzen. Zunächst werden die linguistischen Grundlagen detailliert dargestellt. Dazu gehört neben der Diskussion einiger Definitionen von Sprache ein Überblick über die sprachlichen Evolutionsstufen, eine Übersicht der Bestandteile menschlicher Hochsprachen mitsamt den bekannten Möglichkeiten ihrer Veränderung und eine Übersicht tierischer Sprachen mit kommunikativer Funktion und ihrer Dialektbildung.
Im Anschluss werden die Grundlagen der Informatik und Mathematik erläutert. Diese umfassen neben den Begriffen Modell und Simulation den Aufbau einer Multi-Agenten-Simulation und die Funktionsweise künstlicher neuronaler Netze. Aus den hier genannten Grundlagen wird daraufhin ausführlich das Simulationsmodell dieser Arbeit hergeleitet und beschrieben.
Die Ergebnisse vieler hundert verschiedener Simulationsdurchläufe werden im Anschluss erläutert. So werden die im Modell definierten Störfaktoren einzeln untersucht und in Werteintervalle mit unterschiedlichen Auswirkungen eingeteilt. Weiterhin werden vorhandene Wechselwirkungen der Faktoren aufgezeigt und der Prozess der Sprachwiedervereinigung nach einer vorherigen Dialektspaltung gezeigt.
Einem Fazit und Ausblick folgen als Anhänge Anforderungsdefinition, Entwurf, Architektur, eine detaillierte Erläuterung der Implementierung und ein englischsprachiges Benutzerhandbuch des Werkzeugs DiaLex. DiaLex ist ein komplett in Java konzipiertes und implementiertes Programm und bietet dem Benutzer die Möglichkeit, den Einfluss verschiedener Störfaktoren auf die Dialektbildung innerhalb einer gemeinsam genutzten Sprache einer oder mehrerer Agentengemeinschaften zu simulieren und zu analysieren.
Die Arbeit entstand im Zeitraum Oktober 2007 bis Juni 2010 an der Universität Koblenz-Landau.
Software is vital for modern society. The efficient development of correct and reliable software is of ever-growing importance. An important technique to achieve this goal is deductive program verification: the construction of logical proofs that programs are correct. In this thesis, we address three important challenges for deductive verification on its way to a wider deployment in the industry: 1. verification of thread-based concurrent programs 2. correctness management of verification systems 3. change management in the verification process. These are consistently brought up by practitioners when applying otherwise mature verification systems. The three challenges correspond to the three parts of this thesis (not counting the introductory first part, providing technical background on the KeY verification approach). In the first part, we define a novel program logic for specifying correctness properties of object-oriented programs with unbounded thread-based concurrency. We also present a calculus for the above logic, which allows verifying actual Java programs. The calculus is based on symbolic execution resulting in its good understandability for the user. We describe the implementation of the calculus in the KeY verification system and present a case study. In the second part, we provide a first systematic survey and appraisal of factors involved in reliability of formal reasoning. We elucidate the potential and limitations of self-application of formal methods in this area and give recommendations based on our experience in design and operation of verification systems. In the third part, we show how the technique of similarity-based proof reuse can be applied to the problems of industrial verification life cycle. We address issues (e.g., coping with changes in the proof system) that are important in verification practice, but have been neglected by research so far.
Die Entwicklung von Algorithmen im Sinne des Algorithm Engineering geschieht zyklisch. Der entworfene Algorithmus wird theoretisch analysiert und anschließend implementiert. Nach der praktischen Evaluierung wird der Entwurf anhand der gewonnenen Kenntnisse weiter entwickelt. Formale Verifffizierung der Implementation neben der praktischen Evaluierung kann den Entwicklungsprozess verbessern. Mit der Java Modeling Language (JML) und dem KeY tool stehen eine einfache Spezififfkationssprache und ein benutzerfreundliches, automatisiertes Verififfkationstool zur Verfügung. Diese Arbeit untersucht, inwieweit das KeY tool für die Verifffizierung von komplexeren Algorithmen geeignet ist und welche Rückmeldungen für Algorithmiker aus der Verififfkation gewonnen werden können.Die Untersuchung geschieht anhand von Dijkstras Algorithmus zur Berechnung von kürzesten Wegen in einem Graphen. Es sollen eine konkrete Implementation des Standard-Algorithmus und anschließend Implementationen weiterer Varianten verifffiziert werden. Dies ahmt den Entwicklungsprozess des Algorithmus nach, um in jeder Iteration nach möglichen Rückmeldungen zu suchen. Bei der Verifffizierung der konkreten Implementation merken wir, dass es nötig ist, zuerst eine abstraktere Implementation mit einfacheren Datenstrukturen zu verififfzieren. Mit den dort gewonnenen Kenntnissen können wir dann die Verifikation der konkreten Implementation fortführen. Auch die Varianten des Algorithmus können dank der vorangehenden Verififfkationen verifiziert werden. Die Komplexität von Dijkstras Algorithmus bereitet dem KeY tool einige Schwierigkeiten bezüglich der Performanz, weswegen wir während der Verifizierung die Automatisierung etwas reduzieren müssen. Auf der anderenrn Seite zeigt sich, dass sich aus der Verifffikation einige Rückmeldungen ableiten lassen.
Diese Arbeit stellt ein Werkzeug zur Verfügung, das strukturierte Tests des RIP-MTI Algorithmus vereinfachen, beschleunigen und automatisieren kann. Die vormals zwei Dimensionen Topologie und Updatekonstellation, auf die die MTI-Erweiterung getestet werden musste, konnten auf den variablen Anteil der Topologie vereinfacht werden. Die zeitliche Reihenfolge des Auftretens der Updates kann zentral gesteuert werden. Bisher mussten Tests händisch und sehr aufwändig über Skripte auf der Konsole gesteuert werden. Die entwickelte Testumgebung "XTPeer" ermöglicht es, die gleichen und viele weitere Tests mit kleinem Aufwand durchzuführen.
Confidentiality, integrity, and availability are often listed as the three major requirements for achieving data security and are collectively referred to as the C-I-A triad. Confidentiality of data restricts the data access to authorized parties only, integrity means that the data can only be modified by authorized parties, and availability states that the data must always be accessible when requested. Although these requirements are relevant for any computer system, they are especially important in open and distributed networks. Such networks are able to store large amounts of data without having a single entity in control of ensuring the data's security. The Semantic Web applies to these characteristics as well as it aims at creating a global and decentralized network of machine-readable data. Ensuring the confidentiality, integrity, and availability of this data is therefore also important and must be achieved by corresponding security mechanisms. However, the current reference architecture of the Semantic Web does not define any particular security mechanism yet which implements these requirements. Instead, it only contains a rather abstract representation of security.
This thesis fills this gap by introducing three different security mechanisms for each of the identified security requirements confidentiality, integrity, and availability of Semantic Web data. The mechanisms are not restricted to the very basics of implementing each of the requirements and provide additional features as well. Confidentiality is usually achieved with data encryption. This thesis not only provides an approach for encrypting Semantic Web data, it also allows to search in the resulting ciphertext data without decrypting it first. Integrity of data is typically implemented with digital signatures. Instead of defining a single signature algorithm, this thesis defines a formal framework for signing arbitrary Semantic Web graphs which can be configured with various algorithms to achieve different features. Availability is generally supported by redundant data storage. This thesis expands the classical definition of availability to compliant availability which means that data must only be available as long as the access request complies with a set of predefined policies. This requirement is implemented with a modular and extensible policy language for regulating information flow control. This thesis presents each of these three security mechanisms in detail, evaluates them against a set of requirements, and compares them with the state of the art and related work.
Diese Arbeit bewegt sich im Spannungsfeld dreier Gebiete: Virtualisierung, Echtzeitverarbeitung und Parallelverarbeitung. Jedes dieser Gebiete gilt für sich genommen als weitgehend erforscht, doch ergeben sich bei ihrer gemeinsamen Betrachtung zahlreiche neue Fragestellungen und Möglichkeiten. In dieser Arbeit werden dazu Modelle zur Beschreibung von Echtzeitanwendungen innerhalb der Prozesshierarchie einer Virtualisierungsumgebung entwickelt. Bestehende Schnittstellen zur Virtualisierung werden auf ihre Möglichkeiten zur Echtzeitverarbeitung untersucht, und es werden neue Schnittstellen zur Virtualisierung auf Mehrprozessormaschinen geschaffen und erprobt, die die spezifischen Anforderungen eingebetteter Systeme "insbesondere die Echtzeitfähigkeit" berücksichtigen. Damit wird eine sichere und effiziente Koexistenz von Programmen mit unterschiedlich harten Zeitanforderungen in getrennten virtuellen Maschinen auf einem gemeinsamen Mehrprozessorrechner ermöglicht.