Institut für Informatik
Filtern
Erscheinungsjahr
Dokumenttyp
- Ausgabe (Heft) zu einer Zeitschrift (38)
- Dissertation (35)
- 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
Dualizing marked Petri nets results in tokens for transitions (t-tokens). A marked transition can strictly not be enabled, even if there are sufficient "enabling" tokens (p-tokens) on its input places. On the other hand, t-tokens can be moved by the firing of places. This permits flows of t-tokens which describe sequences of non-events. Their benefiit to simulation is the possibility to model (and observe) causes and effects of non-events, e.g. if something is broken down.
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.