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
- Institut für Informatik (145) (entfernen)
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.
The processing of data is often restricted by contractual and legal requirements for protecting privacy and IPRs. Policies provide means to control how and by whom data is processed. Conditions of policies may depend on the previous processing of the data. However, existing policy languages do not provide means to express such conditions. In this work we present a formal model and language allowing for specifying conditions based on the history of data processing. We base the model and language on XACML.
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.
Ein Netzwerk, wie beispielsweise das Internet, ist eine Menge von Netzen, die durch Router miteinander verbunden sind. Ein Router ist ein Computer, der mit mehreren Netzwerkschnittstellen ausgerüstet und an mehrere Netze angeschlossen ist, um zwischen diesen Pakete zu vermitteln. Man kann ein Netzwerk auch als Graph repräsentieren, wobei Router als Knoten und Netze als Kanten angesehen werden können. Diesen Graph nennt man die Topologie des Netzwerks. Soll ein Paket in ein anderes Netz als das eigene gesendet werden, so wird es normalerweise dem sogenannten Default-Router gesendet. Dieser besitzt (wie jeder Router) eine Tabelle (die sogenannte Forwardingtabelle), die alle Netze enthält. Zusätzlich ist in der Tabelle der jeweilige Router eingetragen, über den das Netz am besten erreicht werden kann. So wird das Paket von einem Router zum nächsten geleitet, bis es das Zielnetz erreicht. Dabei schlägt jeder Router in seiner Tabelle nach, welches der nächste Router auf dem günstigsten Weg zum Zielnetz ist. Ein Routingprotokoll kümmert sich um den automatischen Austausch von Informationen zwischen den Routern, um die Forwardingtabelle aufzubauen und auf dem aktuellen Stand zu halten. Sind die Tabellen aller Router auf dem aktuellen Stand, so befindet sich das Netzwerk in einem konvergenten Zustand. Die Zeit, die benötigt wird, um die Forwardingtabelle aufzubauen beziehungsweise sie nach einer Änderung der Topologie zu aktualisieren, wird Konvergenzzeit genannt. Das Routingprotokoll RIP ist ein bekanntes und gut erforschtes Distanzvektor-Protokoll. Jedoch gibt es bisher nur wenige Untersuchungen der Konvergenzeigenschaften (wie z.B. benötigte Zeit, um in einen konvergenten Zustand zu gelangen, oder das dabei erzeugte Trafficvolumen) dieses Protokolls. Ziel der Arbeit ist es einen Zusammenhang zwischen den Topologieeigenschaften eines Netzwerks und den Konvergenzeigenschaften bei Verwendung des RIP-Routingprotokills experimentell zu ermitteln. Hierfür wurden über 5000 Einzelmessungen mit verschiedenen Topologien durchgeführt und statistisch ausgewertet. Aus den Ergebnissen wurden Formeln abgeleitet, mit deren Hilfe sich für ein beliebiges Netzwerk die Konvergenzeigenschaften anhand seiner Topologieeigenschaften approximieren lassen.
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.
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.
Dieses Dokument schlägt ein Konzept für eine Personal Key Infrastruktur in iCity vor. Über ein Trust Center (TC) ausgestellte Zertiffkate gewährleisten einen sicheren Schlüsselaustausch mit nachweisbarer Authentisierung des Kommunikationspartners, Abhörsicherheit sowie Unverf älschtheit und Nachweisbarkeit der Nachrichten. Das gemeinsam vertrauensw ürdige TC muss während der Kommunikation nicht erreichbar sein. Es erhält lediglich öffentliche Informationen. Das Konzept stellt mehrere Sicherheitsstufen vor, die sichere Identiffkation und Anonymität unterschiedlich gewichten.
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.
Hybrid automata are used as standard means for the specification and analysis of dynamical systems. Several researches have approached them to formally specify reactive Multi-agent systems situated in a physical environment, where the agents react continuously to their environment. The specified systems, in turn, are formally checked with the help of existing hybrid automata verification tools. However, when dealing with multi-agent systems, two problems may be raised. The first problem is a state space problem raised due to the composition process, where the agents have to be parallel composed into an agent capturing all possible behaviors of the multi-agent system prior to the verification phase. The second problem concerns the expressiveness of verification tools when modeling and verifying certain behaviors. Therefore, this paper tackles these problems by showing how multi-agent systems, specified as hybrid automata, can be modeled and verified using constraint logic programming(CLP). In particular, a CLP framework is presented to show how the composition of multi-agent behaviors can be captured dynamically during the verification phase. This can relieve the state space complexity that may occur as a result of the composition process. Additionally, the expressiveness of the CLP model flexibly allows not only to model multi-agent systems, but also to check various properties by means of the reachability analysis. Experiments are promising to show the feasibility of our approach.
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 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.
Cicero ist eine asynchrone Diskussionsplattform, die im Rahmen der Arbeitsgruppe Informationssysteme und Semantic Web (ISWeb) der Universität Koblenz-Landau entwickelt wurde. Die webbasierte Anwendung folgt dem Gedanken eines semantischen Wikis und soll insbesondere beim Arbeitsablauf von Entwurfsprozessen eingesetzt werden. Dabei verwendet Cicero ein restriktives Argumentationsmodell, das einerseits strukturierte Diskussionen von schwierigen Prozessen fördert und andererseits den Entscheidungsfindungsprozess unterstützt. Im Zentrum der Arbeit steht die Evaluation von Cicero, wobei im vorhergehenden theoretischen Teil die Hintergründe und Funktionsweisen vorgestellt werden und im nachfolgenden praktischen Teil die Anwendung anhand einer Fallstudie evaluiert wird. Die Studie wurde im Rahmen der Übungsveranstaltung zu Grundlagen der Datenbanken der Universität Koblenz im Wintersemester 2008/2009 durchgeführt , und die Studenten hatten die Aufgabe, einen Entwurfsprozess mit Hilfe von Cicero zu diskutieren. Über die erhobenen Daten der Fallstudie wird ein Akzeptanztest durchgeführt. Hierbei wird überprüft, ob die Benutzer Cicero positiv annehmen und die Methodik richtig anwenden. Denn aufgrund des vorgegebenen Argumentationsmodells müssen die Benutzer ihr Kommunikationsverhalten ändern und ihren herkömmlichen Diskussionsstil der Anwendung anpassen. Ziel der Evaluation ist es, kritische Erfolgsfaktoren im Umgang mit Cicero ausfindig zu machen. Anhand der identifizierten Schwachstellen werden abschließend gezielte Maßnahmen vorgeschlagen, die die Akzeptanz der Benutzer gegenüber Cicero erhöhen könnten.
An empirical study to evaluate the location of advertisement panels by using a mobile marketing tool
(2009)
The efficiency of marketing campaigns is a precondition for business success. This paper discusses a technique to transfer advertisement content vie Bluetooth technology and collects market research information at the same time. Conventional advertisement media were enhanced by devices to automatically measure the number, distance, frequency and exposure time of passersby, making information available to evaluate both the wireless media as well as the location in general. This paper presents a study analyzing these data. A cryptographic one-way function protects privacy during data acquisition.
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.
Ein Switch (engl. Schalter; auch Weiche) ist eine Netzwerk-Komponente zur Verbindung mehrerer Computer bzw. Netz-Segmente in einem lokalen Netzwerk (LAN). Da Switches den Netzwerkverkehr analysieren und logische Entscheidungen treffen, werden sie auch als intelligente Hubs bezeichnet. Die Funktionsweise eines Switches ist der einer Bridge sehr ähnlich, daher wurde anfangs auch der Begriff Multi-Port-Bridge genutzt 1. Ziel der Diplomarbeit ist es, eine Dokumentation auf die Beine zu stellen, der interessierten Studenten der Informationstechnologie die Möglichkeit bietet, einerseits anhand von physikalischen Switches Administrationsaufgaben nachzuempfinden und andererseits anhand von virtuellen Switches größere Netzwerktopologien aufzubauen. Diese Virtualisierung wird durch das von Virtual Square entwickelte Tool VDE erreicht. Die physikalischen Switches bestehen aus vier Catalyst 3500 XL. Im Laufe dieser Arbeit wird sowohl die Bedienung der einzelnen Systeme untereinander, wie auch die Vernetzung der virtuellen Switches mit den physikalischen Switches erläutert. In diesem Zusammenhang wird auch auf Protokolle und Methoden wie das Spanning Tree Protokoll oder die Virtualisierung eines Netzes durch VLANs eingegangen. Zum Schluss kann der Leser das gelernte in einigen praktischen Aufgaben anwenden.
Hybrid systems are the result of merging the two most commonly used models for dynamical systems, namely continuous dynamical systems defined by differential equations and discrete-event systems defined by automata. One can view hybrid systems as constrained systems, where the constraints describe the possible process flows, invariants within states, and transitions on the one hand, and to characterize certain parts of the state space (e.g. the set of initial states, or the set of unsafe states) on the other hand. Therefore, it is advantageous to use constraint logic programming (CLP) as an approach to model hybrid systems. In this paper, we provide CLP implementations, that model hybrid systems comprising several concurrent hybrid automata, whose size is only straight proportional to the size of the given system description. Furthermore, we allow different levels of abstraction by making use of hierarchies as in UML statecharts. In consequence, the CLP model can be used for analyzing and testing the absence or existence of (un)wanted behaviors in hybrid systems. Thus in summary, we get a procedure for the formal verification of hybrid systems by model checking, employing logic programming with constraints.
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.
Im Rahmen dieser Diplomarbeit wird ein Transaktionskonzept für die aktuelle Implementationsversion der TGraphenbibliothek JGraLab Carnotaurus umgesetzt. Nach einer grundlegenden Einführung in das Konzept der TGraphen werden die relevanten Implementationsdetails der TGraphenbibliothek erläutert. Anschließend erfolgt ein konzeptueller Entwurf, in dem die formalen Grundlagen des Transaktionskonzepts beschrieben werden. Das aus der Datenbankwelt bekannte ACID-Paradigma für Transaktionen dient dabei als wissenschaftliche Grundlage. In einem nächsten Schritt erfolgt der objektorientierte Feinentwurf der Integration des zu entwickelnden Transaktionskonzepts in das vorhandene Gesamtsystem, anhand dessen die Implementation durchgeführt wird. Eine Analyse und Bewertung des umgesetzten Transaktionskonzepts (vor allem im Hinblick auf den Speicherverbrauch und das Laufzeitverhalten) schließen die Arbeit ab.
Performanz von RIP-MTIfi
(2009)
Diese Diplomarbeit beschäftigt sich mit der Performanz von RIP-MTI, insbesondere mit der Performanz der Schleifenerkennung. Ziel der Arbeit ist es, die Zeitdauer der Schleifenerkennung von RIP-MTI zu untersuchen und Probleme, welche bei der Erkennung von Schleifen auftreten könen, aufzudecken und zu lösen.
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.