Filtern
Erscheinungsjahr
Dokumenttyp
- Ausgabe (Heft) zu einer Zeitschrift (38)
- Dissertation (35)
- Diplomarbeit (24)
- Studienarbeit (19)
- Masterarbeit (16)
- Bachelorarbeit (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 (147) (entfernen)
Knowledge compilation is a common technique for propositional logic knowledge bases. The idea is to transform a given knowledge base into a special normal form ([MR03],[DH05]), for which queries can be answered efficiently. This precompilation step is very expensive but it only has to be performed once. We propose to apply this technique to knowledge bases defined in Description Logics. For this, we introduce a normal form, called linkless concept descriptions, for ALC concepts. Further we present an algorithm, based on path dissolution, which can be used to transform a given concept description into an equivalent linkless concept description. Finally we discuss a linear satisfiability test as well as a subsumption test for linkless concept descriptions.
The term "Augmented Reality (AR)" denotes the superposition of additional virtual objects and supplementary information over real images. The joint project Enhanced Reality (ER)1 aims at a generic AR-system. The ER-project is a cooperation of six different research groups of the Department of Computer Science at the University of Koblenz-Landau. According to Ronald Azuma an AR-system combines real and virtual environments, where the real and virtual objects are registered in 3-D, and it provides interactivity in real time [Azu97]. Enhanced Reality extends Augmented Reality by requiring the virtual objects to be seamlessly embedded into the real world as photo-realistic objects according to the exact lighting conditions. Furthermore, additional information supplying value-added services may be displayed and interaction of the user may even be immersive. The short-term goal of the ER-project is the exploration of ER-fundamentals using some specific research scenarios; the long-term goal is the development of a component-based ER-framework for the creation of ER-applications for arbitrary application areas. ER-applications are developed as single-user applications for users who are moving in a real environment and are wearing some kind of visual output device like see-through glasses and some mobile end device. By these devices the user is able to see reality as it is, but he can also see the virtual objects and the additional information about some value-added service. Furthermore he might have additional devices whereby he can interact with the available virtual objects. The development of a generic framework for ER-applications requires the definition of generic components which are customizable and composable to build concrete applications and it requires a homogeneous data model which supports all components equally well. The workgroup "Software Technology"2 is responsible for this subproject. This report gives some preliminary results concerning the derivation of a component-based view of ER. There are several augmented reality frameworks like ARVIKA, AMIRE, DWARF, MORGAN, Studierstube and others which offer some support for the development of AR-applications. All of them ease the use of existing subsystems like AR-Toolkit, OpenGL and others and leverage the generation process for realistic systems by making efficient use of those subsystems. Consequently, they highly rely on them.
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.
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.
Probability propagation nets
(2007)
A class of high level Petri nets, called "probability propagation nets", is introduced which is particularly useful for modeling probability and evidence propagation. These nets themselves are well suited to represent the probabilistic Horn abduction, whereas specific foldings of them will be used for representing the flows of probabilities and likelihoods in Bayesian networks.
In this paper we describe a series of projects on location based and personalised information systems. We start wit a basic research project and we show how we came with the help of two other more application oriented project to a product. This is developed by a consortium of enterprises and it already is in use in the city of Koblenz.
In this paper we describe a network for distributing personalized information within a pervasive university. We discuss the system architecture of our Bluetooth-based CampusNews-system, both, from the administrator and the user viewpoint. We furthermore present first statistical data about the usage of the partial installation at the Koblenz campus together with an outlook to future work.
This paper shows how multiagent systems can be modeled by a combination of UML statecharts and hybrid automata. This allows formal system specification on different levels of abstraction on the one hand, and expressing real-time system behavior with continuous variables on the other hand. It is not only shown how multi-robot systems can be modeled by a combination of hybrid automata and hierarchical state machines, but also how model checking techniques for hybrid automata can be applied. An enhanced synchronization concept is introduced that allows synchronization taking time and avoids state explosion to a certain extent.
Networked RDF graphs
(2007)
Networked graphs are defined in this paper as a small syntactic extension of named graphs in RDF. They allow for the definition of a graph by explicitly listing triples as well as by SPARQL queries on one or multiple other graphs. By this extension it becomes possible to define a graph including a view onto other graphs and to define the meaning of a set of graphs by the way they reference each other. The semantics of networked graphs is defined by their mapping into logic programs. The expressiveness and computational complexity of networked graphs, varying by the set of constraints imposed on the underlying SPARQL queries, is investigated. We demonstrate the capabilities of networked graphs by a simple use case.
Hyper tableaux with equality
(2007)
In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness, but we briefly describe the implementation, too.
UML models and OWL ontologies constitute modeling approaches with different strength and weaknesses that make them appropriate for use of specifying different aspects of software systems. In particular, OWL ontologies are well suited to specify classes using an expressive logical language with highly flexible, dynamic and polymorphic class membership, while UML diagrams are much more suitable for specifying not only static models including classes and associations, but also dynamic behavior. Though MOF based metamodels and UML profiles for OWL have been proposed in the past, an integrated use of both modeling approaches in a coherent framework has been lacking so far. We present such a framework, TwoUse, for developing integrated models, comprising the benefits of UML models and OWL ontologies
In this paper we describe a network for distributing personalized Information in a metropolitan area. We discuss the system architecture of our Bluetooth-based information system as well as the reasoning process that fits users" needs with potential messages. We furthermore present our findings on parallelizing Bluetooth connection setup and performance.
Semantic descriptions of non-textual media available on the web can be used to facilitate retrieval and presentation of media assets and documents containing them. While technologies for multimedia semantic descriptions already exist, there is as yet no formal description of a high quality multimedia ontology that is compatible with existing (semantic) web technologies. We explain the complexity of the problem using an annotation scenario. We then derive a number of requirements for specifying a formal multimedia ontology, including: compatibility with MPEG-7, embedding in foundational ontologies, and modularisation including separation of document structure from domain knowledge. We then present the developed ontology and discuss it with respect to our requirements.
Generalized methods for automated theorem proving can be used to compute formula transformations such as projection elimination and knowledge compilation. We present a framework based on clausal tableaux suited for such tasks. These tableaux are characterized independently of particular construction methods, but important features of empirically successful methods are taken into account, especially dependency directed backjumping and branch local operation. As an instance of that framework an adaption of DPLL is described. We show that knowledge compilation methods can be essentially improved by weaving projection elimination partially into the compilation phase.
This paper offers an informal overview and discussion on first order predicate logic reasoning systems together with a description of applications which are carried out in the Artificial Intelligence Research Group of the University in Koblenz. Furthermore the technique of knowledge compilation is shortly introduced.
The E-KRHyper system is a model generator and theorem prover for first-order logic with equality. It implements the new E-hyper tableau calculus, which integrates a superposition-based handling of equality into the hyper tableau calculus. E-KRHyper extends our previous KRHyper system, which has been used in a number of applications in the field of knowledge representation. In contrast to most first order theorem provers, it supports features important for such applications, for example queries with predicate extensions as answers, handling of large sets of uniformly structured input facts, arithmetic evaluation and stratified negation as failure. It is our goal to extend the range of application possibilities of KRHyper by adding equality reasoning.
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.
SNMP in VNUML Simulationen
(2007)
Das Simple Network Management Protocol (SNMP) gilt als die Universalsprache des Netzwerkmanagements. Bereits Anfang der 90er Jahre wurde die erste Version von SNMP durch die Internet Engineering Task Force (IETF) zum Standard-Internet Management Protocol erklärt und Teil der TCP/IP Protocol-Suite. Für die meisten Betriebssystemplattformen sind SNMP Implementierungen verfügbar und viele netzwerkfähige Geräte und Netzwerkmanagement-Programme unterstützen SNMP, das sich vor allem für die Verwaltung plattformübergreifender und herstellerunabhängiger Netzwerke bewährt. Virtual Network User Mode Linux (VNUML) ist ein mächtiges Netzwerk-Simulationsprogramm für Linux mit dem virtuelle Linux-Rechnernetze aufgebaut werden können, um darin Programmabläufe zu simulieren. Die VNUML Netzwerk-Simulationen sind in erster Linie für das Entwickeln, Analysieren und Testen von Linux Netzwerk-Software, wie zum Beispiel Netzwerk-Protokollen, geeignet. Das Simulationsprogramm entstand im Rahmen des Euro6IX-Projektes, zur Einführung des IPv6 Standards in Europa, am Telematics Engineering Department der Technischen Universität Madrid. Die Rechner der virtuellen Netze, die VNUML aufbaut, basieren auf User Mode Linux (UML), einer in breitem Spektrum eingesetzten Virtualisierung des Linux-Kernels. Diese Studienarbeit beschäftigt sich mit den Möglichkeiten und der Funktionsweise des Netzwerkmanagements mit SNMP. Dafür wird die SNMP-Software Net-SNMP in VNUML Simulationen eingesetzt, um die Möglichkeiten der Konfiguration und des Umgangs mit SNMP in einer praxisnahen Umgebung zu untersuchen. Der Einsatz von Net-SNMP in VNUML Simulationen kann dazu dienen, die Integration von Netzwerkmanagement mit SNMP für relevante Rechnernetze vorzubereiten und Möglichkeiten der Konfiguration und der Verwendung auszuloten oder VNUML Simulationen im Allgemeinen mit diesem bewährten Netzwerkmanagement-System zur Unterstützung auszustatten.
In dieser Arbeit werden einige bekannte Spam Klassiffzierungsmethoden, welche für viele Anwendungen schon im Einsatz sind, kurz erläutert, um sie in einem neuen Szenario zu analysieren. In diesem Szenario wird nicht wie bei E-Mails üblich davon ausgegangen, dass die Nachrichten unbegrenzter Länge sein können, sondern dass es sich hierbei um Nachrichten begrenzter Länge handelt. Auch die Darstellungsform und der vermutliche Inhalt solcher Nachrichten werden aus einem speziellen Kontext heraus betrachtet. So wird davon ausgegangen, dass die Nachrichten auf einem Ticker eines Bildschirmes zu sehen sind, welcher in einer Universität angebracht ist. Somit werden die Nachrichteninhalte sich eher auf das universitäre Umfeld beziehen, wobei angenommen wird, dass die Nachrichteninhalte nur von einer abgeschlossenen Gruppe von Personen eingestellt werden. Nach der Erzeugung einiger Spam- und Hamnachrichten, die auf die Kriterien des Szenarios zutreσfn, werden Klassiffzierungsmethoden evaluiert. Am Ende der Analyse folgt eine Diskussion über die Verwendbarkeit jener Methoden in diesem Szenario. Abgeschlossen wird diese Untersuchung von einem Programm, welches die entsprechenden Methoden zur Klassifizierung implementiert.
In dieser Arbeit wurden insgesamt fünf verwandte, aber variante Definitionen der Hermite-Normalform vorgestellt, angefangen bei der ursprünglichen Version von Charles Hermite. Anschließend wurden vier Basisalgorithmen zur Berechnung der Hermite-Normalform ganzzahliger Matrizen im Detail und anhand von vollständigen Beispielen präsentiert. Hierbei wurde vor allem Wert darauf gelegt, linear-algebraische Grundlagen wie beispielsweise die Verwendung von Permutationsmatrizen für unimodulare Spaltenoperationen verständlich zu vermitteln.
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.
This volume contains those research papers presented at the Second International Conference on Tests and Proofs (TAP 2008) that were not included in the main conference proceedings. TAP was the second conference devoted to the convergence of proofs and tests. It combines ideas from both areas for the advancement of software quality. To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a program is to run it with the expectation of discovering bugs. On the surface, the two techniques seem contradictory: if you have proved your program, it is fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope of proving its correctness. Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools. And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity, but in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of their incompatibility and taking instead the best of what each of these software engineering domains has to offer. The first TAP conference (held at ETH Zurich in February 2007) was an attempt to provide a forum for the cross-fertilization of ideas and approaches from the testing and proving communities. For the 2008 edition we found the Monash University Prato Centre near Florence to be an ideal place providing a stimulating environment. We wish to sincerely thank all the authors who submitted their work for consideration. And we would like to thank the Program Committee members as well as additional referees for their great effort and professional work in the review and selection process. Their names are listed on the following pages. In addition to the contributed papers, the program included three excellent keynote talks. We are grateful to Michael Hennell (LDRA Ltd., Cheshire, UK), Orna Kupferman (Hebrew University, Israel), and Elaine Weyuker (AT&T Labs Inc., USA) for accepting the invitation to address the conference. Two very interesting tutorials were part of TAP 2008: "Parameterized Unit Testing with Pex" (J. de Halleux, N. Tillmann) and "Integrating Verification and Testing of Object-Oriented Software" (C. Engel, C. Gladisch, V. Klebanov, and P. Rümmer). We would like to express our thanks to the tutorial presenters for their contribution. It was a team effort that made the conference so successful. We are grateful to the Conference Chair and the Steering Committee members for their support. And we particularly thank Christoph Gladisch, Beate Körner, and Philipp Rümmer for their hard work and help in making the conference a success. In addition, we gratefully acknowledge the generous support of Microsoft Research Redmond, who financed an invited speaker.
The University of Koblenz-Landau would like to apply for participation in the RoboCup Mixed Reality League in Suzhou, China 2008. Our team is composed of ten team members and two supervisors. All members are graduate students of Computational Visualistics. Our supervisors are Ph.D. candidates currently researching in the working groups of artificial intelligence and computer graphics.
Querying for meta knowledge
(2008)
The Semantic Web is based on accessing and reusing RDF data from many different sources, which one may assign different levels of authority and credibility. Existing Semantic Web query languages, like SPARQL, have targeted the retrieval, combination and reuse of facts, but have so far ignored all aspects of meta knowledge, such as origins, authorship, recency or certainty of data, to name but a few. In this paper, we present an original, generic, formalized and implemented approach for managing many dimensions of meta knowledge, like source, authorship, certainty and others. The approach re-uses existing RDF modeling possibilities in order to represent meta knowledge. Then, it extends SPARQL query processing in such a way that given a SPARQL query for data, one may request meta knowledge without modifying the query proper. Thus, our approach achieves highly flexible and automatically coordinated querying for data and meta knowledge, while completely separating the two areas of concern.
IPv6 Autokonfiguration
(2008)
Diese Studienarbeit stellt verschiedene Möglichkeiten der automatischen Konfiguration von Netzwerkknoten unter IPv6, dem designierten Nachfolger des Internetprotokolls, vor. Dabei wird recht ausführlich in IPv6-Netzwerke eingeführt, wobei aber vorausgesetzt wird, dass der Leser Kenntnisse über das IP-Protokoll der Version 4 hat. Es werden sowohl die zustandslose als auch DHCPv6 ausführlich in der Theorie als auch im praktischen Einsatz gezeigt. Dafür wird das VNUML-System eingesetzt, das an der Technischen Universität Madrid entwickelt wurde und das es ermöglicht, mehrere Linuxsysteme auf einem Wirtsrechner zu simulieren.
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.
Im Rahmen von Projekten haben die Mitarbeiter in einem Unternehmen oft komplexe Problemstellungen zu bearbeiten, für die es keine objektiv richtigen oder falschen Lösungen gibt. Stattdessen werden im Rahmen der Entwurfs- und Entscheidungsprozesse mehrere Lösungsvorschläge erarbeitet um dann unter Abwägung von Pro- und Contra-Argumenten eine möglichst optimale Lösung zu finden.
In dieser Dissertation wird eine Verfahrensweise für die formale Spezifikation und Verifikation von Benutzerschnittstellen unter Sicherheitsaspekten vorgestellt. Mit dieser Verfahrensweise können beweisbar sichere Benutzerschnittstellen realisiert werden. Die Arbeit besteht aus drei Teilen. Im ersten Teil wird eine Methodologie für die formale Beschreibung von Mensch-Maschine-Interaktion entwickelt. Im zweiten Teil werden gängige Computersicherheitskonzepte für die Mensch-Maschine-Interaktion angepasst und mit den im ersten Teil entwickelten Methoden formalisiert. Dabei wird ein generisches formales Modell von Mensch-Maschine-Interaktion erstellt. Im dritten Teil wird die Methodologie, die in den ersten beiden Teilen entwickelt wurde, an einem sicheren Email-Client als exemplarischen Anwendungsprogramm demonstriert.
CAMPUS NEWS - artificial intelligence methods combined for an intelligent information network
(2008)
In this paper we describe a network for distributing personalised information with the usage of artificial intelligence methods. Reception of this information should be possible with everyday mobile equipment. Intelligent filtering and spam protection aim at integrating this technology into our environment. Information on the system architecture and usage of the installation are also presented.
Semantic desktop environments aim at improving the effectiveness and efficiency of users carrying out daily tasks within their personal information management infrastructure (PIM). They support the user by transferring and exploiting the explicit semantics of data items across different PIM applications. Whether such an approach does indeed reach its aim of facilitating users" life and—if so—to which extent, however, remains an open question that we address in this paper with the first summative evaluation of a semantic desktop approach. We approach the research question exploiting our own semantic desktop infrastructure, X-COSIM. As data corpus, we have used over 100 emails and 50 documents extracted from the organizers of a conference-like event at our university. The evaluation has been carried out with 18 subjects. We have developed a test environment to evaluate COSIMail and COSIFile, two semantic PIM applications based on X-COSIM. As result, we have found a significant improvement for typical PIM tasks compared to a standard desktop environment.
Simulation mit VNUML
(2008)
Diese Studienarbeit soll als Einführung in das Thema Netzwerksimulation dienen und unter anderem auch als Einstiegs-Referenz für zukünftige Besucher der Rechnernetze-Veranstaltungen an der Universität Koblenz nutzbar sein. Die Ausarbeitung beginnt mit den Grundlagen zu UML und VNUML und beschreibt dann die Installation, Konfiguration und das Arbeiten mit dem Netzwerksimulator sowie oft genutzter Tools. Im Anschluss daran werden konkrete Anwendungsfelder vorgestellt: der simulierte Einsatz des Paketfilter iptables zur Realisierung von Firewalls und NAT, verschiedene Netzwerkdienste und zuguterletzt simuliertes Routing mit der quagga-Suite.
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.
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.
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.
The lack of a formal event model hinders interoperability in distributed event-based systems. Consequently, we present in this paper a formal model of events, called F. The model bases on an upper-level ontology and pro-vides comprehensive support for all aspects of events such as time and space, objects and persons involved, as well as the structural aspects, namely mereological, causal, and correlational relationships. The event model provides a flexible means for event composition, modeling of event causality and correlation, and allows for representing different interpretations of the same event. The foundational event model F is developed in a pattern-oriented approach, modularized in different ontologies, and can be easily extended by domain specifific ontologies.
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.
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.
Avoidance of routing loops
(2009)
We introduce a new routing algorithm which can detect routing loops by evaluating routing updates more thoroughly. Our new algorithm is called Routing with Metric based Topology Investigation (RMTI), which is based on the simple Routing Information Protocol (RIP) and is compatible to all RIP versions. In case of a link failure, a network can reorganize itself if there are redundant links available. Redundant links are only available in a network system like the internet if the topology contains loops. Therefore, it is necessary to recognize and to prevent routing loops. A routing loop can be seen as a circular trace of a routing update information which returns to the same router, either directly from the neighbor router or via a loop topology. Routing loops could consume a large amount of network bandwidth and could impact the endtoend performance of the network. Our RMTI approach is capable to improve the efficiency of Distance Vector Routing.
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.
Rechnernetze gehört zu den Fächern, die ein breites Spektrum an Anwendungsgebieten abdecken. Die vielen unterschiedlichen Protokolle sind Belege dafür. Jedes Protokoll hat sozusagen ein eigenes Anwendungsbereich und doch sind deren Aufgaben unter dem Nenner gleich. Miteinander zu Kommunizieren, Informationen auszutauschen und das möglichst auf eine sichere und schnelle Art und Weise. Als Beispiel denke man an Autos, Handys, Lokale Netze in einem kleinen Betrieb, Intranet in einer größeren Organisation oder in Netze die über Länder hinweggehen. Ein modernes Auto an sich hat schon eine Vielzahl an Bussystemen in sich integriert. CAN, LIN, FlexRay oder MOST Bus sind ein paar Stichworte dazu. Wenn man jetzt von der Autoindustrie weggeht und an die Autonomen Systeme kommt, gibt es dort ein Routing Information Protokoll, das innerhalb von Autonomen Systemen verwendet wird. Routing Information Protokoll ist eines der meist verwendeten Protokolle innerhalb von Autonomen Systemen. Das Routing Information Protokoll ist einer der zentralen Bestandteile des Forschungsbereiches der AG Steigner. Die Arbeit widmet sich unter Anderem dieser Forschungsunterstützung.Diese Studienarbeit hat das Ziel die Testumgebung XTPeer auf die VNUML Version 1.8 zu integrieren.
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.
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.
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.
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.
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.
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.
Bislang wurde VNUML (Virtual Network User Mode Linux) innerhalb der AG Rechnernetze der Uni Koblenz dazu verwendet, um die eigene Protokollerweiterung zu RIP, RIP/MIT (RIP with minimal topology information), auf Stärken und Schwächen zu testen. Hauptsächlich wurden dafür spezielle Testszenarien verwendet, um zu untersuchen, ob ein Count-to-Infinity-Problem (CTI) erfolgreich verhindert wird und wie schnell das Netz nach Ausfall einer Route konvergiert. Diese Arbeit wird untersuchen, ob die MTI-Erweiterung auch Performance-Vorteile in größeren Netzwerken bietet, ob sich der Einsatz des Script-Tools EDIV (spanisch: Escenarios DIstribuidos con VNUML, englisch: Distributed Scenarios using VNUML) aufgrund der besseren Skalierbarkeit lohnt und ob sich durch die Verteilung eines XML-Szenarios auf mehrere Rechner signifikant auf die Konvergenzzeit auswirkt. Dazu werden neben Simulationen auch Testszenarien entworfen und umfangreichen Tests unterzogen, um Erkenntnisse zur Effizienz und Skalierbarkeit des Distance Vector Routing Protokolls RIP/MTI zu ziehen.