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)
- XTPeer (3)
- Campus Information System (2)
- Drahtloses Sensorsystem (2)
- Equality (2)
- Information Retrieval (2)
- Konvergenz (2)
- Modellgetriebene Entwicklung (2)
- Network (2)
- Ontology (2)
- Petri-Netze (2)
- Prädikatenlogik (2)
- RIP (2)
- Rechnernetz (2)
- Theorem Proving (2)
- UML (2)
- University (2)
- constraint logic programming (2)
- hybrid automata (2)
- probability propagation nets (2)
- API (1)
- API analysis (1)
- API-Analyse (1)
- AUTOSAR (1)
- Abduktion <Logik> (1)
- Ad-hoc-Netz (1)
- Adaptation (1)
- Administration (1)
- Algorithm Engineering (1)
- Algorithmische Geometrie (1)
- Anpassung (1)
- Architektur <Informatik> (1)
- Auditing (1)
- Augmented Reality (1)
- Aussagenlogik (1)
- Authentisierung (1)
- Automated Theorem Proving (1)
- Automated Theorem Proving Systems (1)
- Automatisches Beweisverfahren (1)
- Automotive Systems (1)
- Backtrack (1)
- Bayes Procedures (1)
- Beaconless (1)
- Befahrbarkeit (1)
- Betriebssystem (1)
- Border Gateway Protocol (1)
- Border Gateway Protocol 4 (1)
- C-Socketbibliothek (1)
- CMS (1)
- CSCA (1)
- CTI (1)
- CTI -Problem (1)
- Calculus (1)
- Cheops (1)
- Cicero (1)
- Circumscription (1)
- Cisco Catalyst 3500XL (1)
- Communication Networks (1)
- Computational logic (1)
- Computer Security (1)
- Computer Supported Cooperative Work (1)
- Computersicherheit (1)
- Computersimulation (1)
- Conference (1)
- Connected Vehicles (1)
- Context-aware processes (1)
- Controlling (1)
- Counting-to-Infinity (1)
- DHCPv6 (1)
- DNNF (1)
- DPLL (1)
- DPLL procedure (1)
- Data Mining (1)
- Datenschutz (1)
- Deduktion (1)
- Description Logics (1)
- Destiny (1)
- Developer profiling (1)
- DiaLex (1)
- Dialekt (1)
- Dijkstras Algorithmus (1)
- Dimension 3 (1)
- Diskrete Simulation (1)
- Distanz-Vektor (1)
- Distributed Algorithm (1)
- Distributed Environments (1)
- Distributed process execution (1)
- Dokumentation (1)
- Drahtloses vermachtes Netz (1)
- Driver Assistance Systems (1)
- E-Participation (1)
- Ebener Graph (1)
- Echtzeit-Interaktion (1)
- Echtzeitsysteme (1)
- Empirical Studies (1)
- Emulation (1)
- Enhanced Reality (1)
- Enterprise Architecture Framework (1)
- Entscheidungsprozess (1)
- Entwickler Profil (1)
- Fahrerassistenzsysteme (1)
- Fahrzeug (1)
- Fließgewässer (1)
- Flowing Inland Waters (1)
- Formal Methods (1)
- Formale Methoden (1)
- Formale Ontologie (1)
- Fragebeantwortung (1)
- GPS (1)
- GReTL (1)
- Gelände (1)
- Geographic routing (1)
- Geometric spanner (1)
- Graph (1)
- Grounded Theory (1)
- HNF-Algorithmus (1)
- Hermite-Normalform (1)
- Heuristiken (1)
- Hindernis (1)
- Horn Clauses (1)
- Human-Computer Interaction (1)
- Hyper Tableau Calculus (1)
- IASON (1)
- IPv6 (1)
- IT Guru (1)
- IT-Security (1)
- Information (1)
- Information Centric Networking (1)
- Information Visualization (1)
- Informationsverlinkung (1)
- Informationsvisualisierung (1)
- InstaHub (1)
- Intelligent Information Network (1)
- Interactive Video Retrieval (1)
- Interactive Visualizations (1)
- Interaktive Visualisierungen (1)
- Interior Gateway Protokoll (1)
- JGraLab (1)
- JML (1)
- Java (1)
- Java Modeling Language (1)
- Java. Programmiersprache (1)
- KRHyper (1)
- Klassifikation (1)
- Klausellogik (1)
- Knowledge (1)
- Knowledge Engineering (1)
- Komplexität / Algorithmus (1)
- Laser (1)
- Linking of Information (1)
- Linux (1)
- Local algorithm (1)
- Logischer Schluss (1)
- Lookup-Algorithmen (1)
- MIA (1)
- MPEG-7 (1)
- MSR (1)
- Mail-Filter (1)
- Mehrprozessorsystem (1)
- Mensch-Maschine-Interaktion (1)
- Metamodel (1)
- Meteor (1)
- Metriken (1)
- Mikrocontroller (1)
- Mining (1)
- Mining Software Repositories (1)
- Mobile Information Systems (1)
- Mobiltelefon (1)
- Modelltransformation (1)
- Monitoring (1)
- Multi-Agenten-Simulation (1)
- Multi-robot System (1)
- Multiagent System (1)
- Multiagentensysteme (1)
- Nachbarschaftsgraph (1)
- Nagios (1)
- Named Function Networking (1)
- Network Monitoring (1)
- Network Simulation (1)
- Netzwerk Protokollen (1)
- Netzwerkanalyse (1)
- Netzwerkchip (1)
- Netzwerkmanagment (1)
- Netzwerktopologie (1)
- Netzwerküberwachung (1)
- Neuronales Netz (1)
- Nutzerzufriedenheit (1)
- OPNET (1)
- OWL <Informatik> (1)
- Ontologie <Wissensverarbeitung> (1)
- OpenWrt (1)
- Oracle Generation (1)
- Oraklegenerierung (1)
- Orientierungsstufe (1)
- PDA (1)
- Personal Key Infrastruktur (1)
- Personalised Information Systems (1)
- Petri Nets (1)
- Petri net (1)
- Petrinetz (1)
- Placement Strategies (1)
- Planar graphs (1)
- Policy Language (1)
- Proactive Caching (1)
- Probability (1)
- Probability propagation nets (1)
- Einbringen (1)
- Process tracing (1)
- Projekt iCity (1)
- Propagation (1)
- Propositional Logic (1)
- Protocol (1)
- Prototyp (1)
- Prototype (1)
- Provenance (1)
- Quasi unit disk graph (1)
- Query Expansion (1)
- RDF Graphs (1)
- RDF modeling (1)
- RIP-MTI Algorithmus (1)
- RMTI (1)
- Reactive algorithm (1)
- Rechnernetze (1)
- Reference Model (1)
- Relationale Datenbank (1)
- Relevance Feedback (1)
- Requirement-Engineering (1)
- Resource Description Framework (RDF) (1)
- Robocup 2008 (1)
- Roboter (1)
- Router (1)
- Routing Information Protocol (1)
- Routing Information Protocol (RIP) (1)
- Routing Loops (1)
- Routing information protocol (1)
- Routing with Metric based Topology Investigation (RMTI) (1)
- Routing- und Forwarding Tabellen (1)
- Routing-Loop (1)
- SAC (1)
- SNMP (1)
- SOA (1)
- SPARQL (1)
- STP (1)
- Schleifenerkennung (1)
- Schlussfolgern (1)
- Security Requirements (1)
- Semantic Web Data (1)
- Semantics (1)
- Semantisches Wiki (1)
- Serdar Ayalp (1)
- Serviceorientierte Architektur (1)
- Software Language (1)
- Software Repositories (1)
- Software Technology (1)
- Softwarearchitektur (1)
- Softwaretest (1)
- Softwaretesting (1)
- Soziale Netzwerke (1)
- Spam-Mail (1)
- Spannender Baum (1)
- Spanning Tree (1)
- Specification (1)
- Spezifikation (1)
- Statistische Analyse (1)
- Stochastic Logic (1)
- Straßenzustand (1)
- Suat Algin (1)
- TAP (1)
- TGraph (1)
- TRECVID (1)
- Tableau <Logik> (1)
- Tableau Calculus (1)
- Technologischer Raum (1)
- Technology Acceptance Model (1)
- Temperaturmessung (1)
- Test Generation (1)
- Testgenerierung (1)
- Theorem prover (1)
- Theorembeweiser (1)
- Tokens (1)
- Transaction concept (1)
- Transaktion (1)
- Transaktionskonzept (1)
- Ultraschall (1)
- Unified Modeling Language (UML ) (1)
- Unit disk graph (1)
- VDE (1)
- VDE-Switch (1)
- VLAN (1)
- VTP (1)
- Vegetation distribution (1)
- Verifikation (1)
- Verortung (1)
- Verteilter Algorithmus (1)
- Virtual Square (1)
- Virtual network user mode Linux (1)
- Virtualisation (1)
- Virtualisierung (1)
- Visualisierung (1)
- Wahrscheinlichkeitsrechnung (1)
- Wasseroberfläche (1)
- Water Surface Temperature (1)
- Web Ontology Language (OWL) (1)
- Werbung (1)
- Wiki (1)
- Wireless Sensor Networks (1)
- Wireless sensor network (1)
- Wireshark (1)
- Wissenskompilation (1)
- Wissensmanagement (1)
- World Wide Web (1)
- World Wide Web 2.0 (1)
- XML (1)
- XML-Dokument (1)
- Zertifikat (1)
- Zirkumskription (1)
- Zusammenhängender Graph (1)
- andLinux (1)
- andLinux. (1)
- automated theorem prover (1)
- backpropagation (1)
- bias (1)
- classification (1)
- concurrency (1)
- convergence analysis (1)
- data mining (1)
- deductive (1)
- description logic (1)
- e-learning (1)
- e-service quality (1)
- ediv (1)
- event model (1)
- event-based systems (1)
- first-order logic (1)
- folksonomies (1)
- gaze information (1)
- grassland (1)
- hybrid systems (1)
- hybride Automaten (1)
- iCity project (1)
- image semantics (1)
- information retrieval (1)
- knowledge management system (1)
- landmarks (1)
- living book (1)
- model generation (1)
- multi-agent systems (1)
- multiagent systems (1)
- multiprocessing (1)
- networks (1)
- neural (1)
- ontology (1)
- parallel computing (1)
- personal information management (1)
- persönliches Informationsmanagement (1)
- privacy protection (1)
- public key infrastructure (1)
- question answering (1)
- real-time computing (1)
- reasoning (1)
- recurrent (1)
- rip (1)
- rmti (1)
- semantic desktop (1)
- semantics (1)
- semantischer Desktop (1)
- sequent calculi (1)
- simulation (1)
- summative evaluation (1)
- tag recommendation (1)
- tagging (1)
- vegetation modeling (1)
- verification (1)
- virtual network user mode linux (1)
- vnuml (1)
- web 2.0 (1)
- xtpeer (1)
Institut
- Institut für Informatik (145) (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.
The trends of industry 4.0 and the further enhancements toward an ever changing factory lead to more mobility and flexibility on the factory floor. With that higher need of mobility and flexibility the requirements on wireless communication rise. A key requirement in that setting is the demand for wireless Ultra-Reliability and Low Latency Communication (URLLC). Example use cases therefore are cooperative Automated Guided Vehicles (AGVs) and mobile robotics in general. Working along that setting this thesis provides insights regarding the whole network stack. Thereby, the focus is always on industrial applications. Starting on the physical layer, extensive measurements from 2 GHz to 6 GHz on the factory floor are performed. The raw data is published and analyzed. Based on that data an improved Saleh-Valenzuela (SV) model is provided. As ad-hoc networks are highly depended onnode mobility, the mobility of AGVs is modeled. Additionally, Nodal Encounter Patterns (NEPs) are recorded and analyzed. A method to record NEP is illustrated. The performance by means of latency and reliability are key parameters from an application perspective. Thus, measurements of those two parameters in factory environments are performed using Wireless Local Area Network (WLAN) (IEEE 802.11n), private Long Term Evolution (pLTE) and 5G. This showed auto-correlated latency values. Hence, a method to construct confidence intervals based on auto-correlated data containing rare events is developed. Subsequently, four performance improvements for wireless networks on the factory floor are proposed. Of those optimization three cover ad-hoc networks, two deal with safety relevant communication, one orchestrates the usage of two orthogonal networks and lastly one optimizes the usage of information within cellular networks.
Finally, this thesis is concluded by an outlook toward open research questions. This includes open questions remaining in the context of industry 4.0 and further the ones around 6G. Along the research topics of 6G the two most relevant topics concern the ideas of a network of networks and overcoming best-effort IP.
Das Routing Information Protocol (RIP) ist ein Internet-Standard-Routing-Protokoll, das einst mit zu den am meisten eingesetzten Routing-Protokollen in IP-Netzwerken gehörte. Es basiert auf dem sogenannten Distanzvektoralgorithmus und ist in seiner Funktion und seinem Aufbau sehr einfach ausgelegt. Seit jeher leidet es allerdings unter dem sogenannten Counting-to-Infinity (CTI) Problem, bei dem die Erreichbarkeit einer eigentlich ausgefallenen Verbindung zu einem Ziel scheinbar aufrechterhalten wird. Die Distanz zu diesem Ziel wird aufgrund des fortwährenden Austauschs von nicht mehr gültigen Verbindungsinformationen zwischen in einem Ring geschalteten RIP-Routern hochgezählt, theoretisch bis ins Unendliche. Dabei entstehen Routingschleifen, die den Netzwerkbetrieb erheblich stören können, da die gesendeten Netzwerkpakete aufgrund der Schleife die selben Router immer wieder passieren und weder an ihr eigentliches Ziel gelangen noch verworfen werden können. Die Gefahr des Auftretens des CTI-Problems schränkt die Einsetzbarkeit von RIP enorm ein. Die Netzwerke, in denen RIP eingesetzt wird, können nicht beliebig wachsen, da die maximale Größe des Netzwerks auf eine relativ kleine Distanz zwischen den Routern begrenzt ist, um die Dauer und die Folgen des CTI-Problems im Falle des Auftretens gering zu halten. Je stärker auch die Topologie eines Netzwerks vermascht ist, um mit zusätzlichen, alternativen Verbindungen Ausfällen entgegenzuwirken, umso stärker steigt auch die Gefahr des Auftretens des CTI-Problems nach einem Ausfall. Bislang existierten für RIP lediglich Mechanismen, die das Risiko des Auftretens und die Auswirkungen des CTI-Problems verringern, das Problem selbst aber nicht beheben können. Mit "RIP with minimal topology information" (RIP-MTI) wurde in der AG Rechnernetze an der Universität Koblenz-Landau eine abwärtskompatible Erweiterung zu RIP geschaffen, die das CTI-Problem zu beheben verspricht. Der RIP-MTI-Algorithmus sammelt zusätzliche Informationen über die Topologie des Netzwerks und nutzt diese, um nach dem Ausfall einer Verbindung richtige Informationen über die Erreichbarkeit von Zielen von falschen Informationen unterscheiden zu können. In dieser Diplomarbeit wird die Implementierung des RIP-MTI-Algorithmus behandelt. Mit Hilfe der speziell entwickelten RIP-Netzwerk-Testumgebung XTPeer, in der das CTI-Problem kontrolliert provoziert werden kann, wird die Wirksamkeit der Implementierung eines Quagga RIP-MTI-Routers überprüft und entsprechend weiterentwickelt. Dafür wird der RIP-MTI-Algorithmus an die Implementierung des Quagga RIP-Routing-Software sowie an die der Netzwerk-Testumgebung XTPeer angepasst. Diese Diplomarbeit wird vom Autor selbst als fortgeschrittene Zwischenstation eingestuft, vor der Herstellung und Herausgabe der Implementierung einer RIP-MTI-Routing-Software, die auch in produktiven Netzwerken eingesetzt werden könnte.
In unserer heutigen Welt spielen soziale Netzwerke eine immer größere werdende Rolle. Im Internet entsteht fast täglich eine neue Anwendung in der Kategorie Web 2.0. Aufgrund dieser Tatsache wird es immer wichtiger die Abläufe in sozialen Netzwerken zu verstehen und diese für Forschungszwecke auch simulieren zu können. Da alle gängigen sozialen Netzwerke heute nur im eindimensionalen Bereich arbeiten, beschäftigt sich diese Diplomarbeit mit mehrdimensionalen sozialen Netzwerken. Mehrdimensionale soziale Netzwerke bieten die Möglichkeit verschiedene Beziehungsarten zu definieren. Beispielsweise können zwei Akteure nicht nur in einer "kennt"-Beziehung stehen, sondern diese Beziehungsart könnte auch in diverse Unterbeziehungsarten, wie z.B. Akteur A "ist Arbeitskollege von" Akteur B oder Akteur C "ist Ehepartner von" Akteur D, unterteilt werden. Auf diese Art und Weise können beliebig viele, völlig verschiedene Beziehungsarten nebeneinander existieren. Die Arbeit beschäftigt sich mit der Frage, in welchem Grad die Eigenschaften von eindimensionalen auch bei mehrdimensionalen sozialen Netzwerken gelten. Um das herauszufinden werden bereits bestehende Metriken weiterentwickelt. Diese Metriken wurden für eindimensionale soziale Netzwerke entwickelt und können nun auch für die Bewertung mehrdimensionaler sozialer Netzwerke benutzt werden. Eine zentrale Fragestellung ist hierbei wie gut sich Menschen finden, die sich etwas zu sagen haben. Um möglichst exakte Ergebnisse zu erhalten, ist es notwendig reale Daten zu verwenden. Diese werden aus einem Web 2.0-Projekt, in das Benutzer Links zu verschiedenen Themen einstellen, gewonnen (siehe Kapitel 4). Der erste praktische Schritte dieser Arbeit besteht daher darin, das soziale Netzwerk einzulesen und auf diesem Netzwerk eine Kommunikation, zwischen zwei Personen mit ähnlichen Themengebieten, zu simulieren. Die Ergebnisse der Simulation werden dann mit Hilfe der zuvor entwicklelten Metriken ausgewertet.
Die Motivation für diese Arbeit bestand darin, den Studierenden in den Rechnerpools der Universität Koblenz die Möglichkeit zu geben, mit der Simulationssoftware VNUML (Virtual Network User Mode Linux) zu arbeiten. Eingesetzt wird diese Software in den Vorlesungen und Übungen zu Rechnernetzen I und II, was eine Anwendung der Software für die Studenten unumgänglich macht. In der Vergangenheit gab es jedoch immer wieder Probleme bei der Installation und Einrichtung auf den privaten Rechnern, obwohl in früheren Studienarbeiten mehrfach vereinfachte Installationsroutinen entwickelt worden waren. Ein weiteres Problem für die Verwendung von VNUML stellt auch die Tatsache dar, dass die Software nur in einer Linux-Umgebung lauffähig ist. Da aber nicht alle Studierenden das Betriebssystem Linux benutzen und viele vor einer Installation allein zur Verwendung von VNUML zurückschrecken, war es schon länger angedacht, diese Software an den Rechnern der Universität zur Verfügung zu stellen. In dieser Arbeit wird der Prozess beschrieben, wie eine Installation der VNUML-Software in den Rechnerpools möglich war, welche Probleme dabei aufgetreten sind und welche Alternativen zur gewählten Vorgehensweise möglich gewesen wären. Das Ergebnis bietet auch eine sehr einfache Installation für den privaten Anwender, ohne dass hierfür eine eigenständige Linux-Installation nötig wäre. Auch wurden während der Entwicklung immer weitere Verbesserungen vorgenommen, welche die Anwenderfreundlichkeit der endgültigen Lösung weiter erhöhten. Die Möglichkeiten und Ideen sind dabei auch so vielfältig, dass sich die Arbeitsgruppe noch weiter mit diesem Thema beschäftigen wird und weitere Optimierungen vorgenommen werden können.
Wireshark und VNUML Im Rahmen dieser Studienarbeit sollen einige Netzwerk-Protokolle mit dem Protokollanalyser Wireshark beobachtet und der Umgang damit beschrieben werden. Wireshark ist ein Ableger von "Ethereal", einem der bekanntesten Protokoll-Analyser. Wireshark analysiert Netzwerkverkehr, zeichnet ihn auf und stellt ihn übersichtlich dar. Für die Simulation des Netzwerks wird VNUML verwendet. Da VNUML nur unter Linux verwendet werden kann, wird andLinux als virtuelle Maschine dazwischen geschaltet um auch in Windows arbeiten zu können.
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.
Diese Studienarbeit soll eine Einführung in die Arbeit mit virtual network user mode linux (VNUML) geben. Mit Hilfe dieser Arbeit möchte ich speziell die Version VNUML 1.6 näher bringen und die wesentlichen Unterschiede, Vor- und Nachteile zur Version 1.5 zeigen. In den nächsten zwei Kapiteln wird auf das Thema VNUML und UML oberflächlich eingegangen. Das darauffolgende Kapitel befasst sich mit der Installation von VNUML 1.6, der Vorraussetzung und den möglichen Fehlermeldungen. Wenn dies abgeschlossen ist, wird VNUML 1.6 mit eigenen Beispielen ausfürlich, praktisch und theoretisch vorgestellt. Danach werden die wesentlichen Unterschiede von VNUML 1.5 zu VNUML 1.6 beschrieben. Zum Abschluss sind noch ein Kapitel mit kurzen Begriffsdefinitionen und der Anhang mit allen XML-Dateien zu finden. Auf den Aufbau einer XML-Datei möchte ich in meiner Arbeit nicht weiter eingehen. Dazu verweise ich auf die Arbeit von Thomas Chmielowiec und Tim Keupen. In diesen Arbeiten sind die XML-Syntax und Semantik ausfürlich beschrieben.
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.