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)
The model evolution calculus
(2004)
The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.
The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and selfdetermined learning in lectures, tutorials and self study. The Living Book includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. This paper describes the Living Book and the use of theorem proving technology as a core component in the knowledge management system (KMS) of the Living Book. The KMS provides a scenario management component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called 'slices' (definitions, theorems, and so on) in a scenario-based way (like 'I want to prepare for an exam and need to learn about resolution'). The computation of such assemblies is carried out by a model-generating theorem prover for first-order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-programming style rules that describe the scenario-specific composition of slices. Additionally, a user model is taken into account that contains information about topics and slices that are known or unknown to a student. A model computed by the system for such input then directly specifies the document to be assembled. This paper introduces the elearning context we are faced with, motivates our choice of logic and presents the newly developed calculus used in the KMS.
We aim to demonstrate that automated deduction techniques, in particular those following the model computation paradigm, are very well suited for database schema/query reasoning. Specifically, we present an approach to compute completed paths for database or XPath queries. The database schema and a query are transformed to disjunctive logic programs with default negation, using a description logic as an intermediate language. Our underlying deduction system, KRHyper, then detects if a query is satisfiable or not. In case of a satisfiable query, all completed paths -- those that fulfill all given constraints -- are returned as part of the computed models. The purpose of our approach is to dramatically reduce the workload on the query processor. Without the path completion, a usual XML query processor would search the database for solutions to the query. In the paper we describe the transformation in detail and explain how to extract the solution to the original task from the computed models. We understand this paper as a first step, that covers a basic schema/query reaÂsoning task by model-based deduction. Due to the underlying expressive logic formalism we expect our approach to easily adapt to more sophisticated problem settings, like type hierarchies as they evolve within the XML world.
Fehler in der Anforderungsanalyse führen häufig zu Misserfolgen in der Entwicklung von Softwaresystemen. Seit einiger Zeit wird versucht, diesem Problem durch Requirements- Engineering zu begegnen. Durch die frühe Beteiligung aller Stakeholder an der Entwicklung eines Systems sowie eine strukturierte Vorgehensweise zur Ermittlung und Analyse von Anforderungen an ein zu erstellendes System hat es als erster Schritt in der Entwicklung von Softwaresystemen zunehmend an Bedeutung gewonnen. Die steigende Komplexität moderner Softwaresysteme bringt jedoch eine gewaltige Menge an Informationen mit sich, die während der Analyse erfasst und verwaltet werden müssen. Dieser Informationsflut ist ohne Unterstützung durch entsprechende Software kaum beizukommen. Vor allem in größeren, räumlich verteilten Projekten wäre ein effektives Requirements-Engineering sonst kaum möglich. Es gibt inzwischen eine Vielzahl von Tools, die das Requirements-Engineering unterstützen. Diese Tools sind bereits seit geraumer Zeit im Einsatz und setzen in ihren aktuellsten Versionen die wichtigsten Konzepte des Requirements-Engineering um. Im Rahmen dieser Arbeit werden einige dieser Tools im Hinblick auf Funktionsumfang und Verzeichnisstruktur untersucht. Besonderes Interesse galt der Verwaltung von Anforderungen und deren Abhängigkeiten untereinander. Die gewonnenen Erkenntnisse werden anschließend in ein Referenzmodell integriert.
Interactive video retrieval
(2006)
The goal of this thesis is to develop a video retrieval system that supports relevance feedback. One research approach of the thesis is to find out if a combination of implicit and explicit relevance feedback returns better retrieval results than a system using explicit feedback only. Another approach is to identify a model to weight existing feature categories. For this purpose, a state-of-the-art analysis is presented and two systems implemented, which run under the conditions of the international TRECVID workshop. It will be a basis system for further research approaches in the field of interactive video retrieval. Amongst others, it shall participate in the 2006 search task of the mentioned workshop.
Die hohen Infrastrukturkosten machen das Überprüfen von Theorien bezüglich großer Rechnernetze zu einer schwierigen und teuren Aufgabe. Ein möglicher Ansatz dieses Problem zu beheben ist die Verwendung von virtueller anstelle von physikalischer Infrastrukur. OPNets IT Guru ist ein Programm, das entworfen wurde zur Simulation großer Netze und zur Repräsentation relevanter Informationen. Es gestattet großflächige Änderungen zu testen oder Theorien zu überpruefen ohne den Aufwand einer physikalischen Infrastruktur.
Partielle Wissenskompilation
(2006)
Viele Probleme in der Aussagenlogik sind nur sehr aufwändig lösbar. Ist beispielsweise eine Wissensbasis gegeben, an die wir Anfragen stellen, wollen, so kann dies mitunter sehr mühsam sein. Um trotzdem effizient Anfragen beantworten zu können, hat sich die Vorgehensweise der Wissenskompilation entwickelt. Dabei wird die Lösung der Aufgabe in eine Offline- und eine Online-Phase aufgeteilt. In der Offline-Phase wird die Wissensbasis präkompiliert. Dabei wird sie in eine bestimmte Form umgewandelt, auf der sich die erwarteten Anfragen effizient beantworten lassen. Diese Transformation der Wissensbasis ist meist sehr aufwändig, muss jedoch nur einmalig durchgeführt werden. In der darauffolgenden Online-Phase können nun effizient Anfragen beantwortet werden. In dieser Diplomarbeit wird eine spezielle Normalform, die sich als Zielsprache der Präkompilation anbietet, untersucht. Außerdem wird die Präkompilation so in einzelne Schritte unterteilt, dass möglicherweise bereits nach einigen Teilschritten Anfragen beantwortet werden können.
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.
Die vorliegende Arbeit stellt eine Methode für die korpusbasierte Analyse der Verwendung von Softwarebibliotheken in Java-Programmen vor. Die meisten größeren Softwareprojekte verwenden Softwarebibliotheken, die als Schnittstelle für den Programmierer sogenannte APIs (application programming interfaces) bereitstellen. Um den Umstieg von einer solchen API auf eine andere zu unterstützen, strebt man Werkzeuge zur automatisierten API-Migration an. Zur Entwicklung solcher Werkzeuge fehlen allerdings noch Basisdaten. Statistiken und Beobachtungen zur Verwendung von APIs in der Praxis wurden bisher nur mit sehr kleinen Korpora von Projekten und APIs durchgeführt. Wir stellen in dieser Arbeit daher eine Analysemethode vor, die für Messungen an großen Korpora geeignet ist. Hierzu erzeugen wir zunächst einen Korpus von auf SourceForge gehosteten Open-Source-Projekten sowie einen Korpus von Softwarebibliotheken. In der Folge werden alle Projekte des Korpus compiliert, wobei ein Compiler-Plugin für den javac detaillierte Informationen über jede einzelne Methode liefert, die der Compiler erstellt. Diese Informationen werden in einer Datenbank gespeichert und analysiert.
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.
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.
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.
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.
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.
This thesis introduces fnnlib, a C++ library for recurrent neural network simulations that I developed between October 2009 and March 2010 at Osaka University's Graduate School of Engineering. After covering the theory behind recurrent neural networks, backpropagation through time, recurrent neural networks with parametric bias, continuous-time recurrent neural networks, and echo state networks, the design of the library is explained. All of the classes as well as their interrelationships are presented along with reasons as to why certain design decisions were made. Towards the end of the thesis, a small practical example is shown. Also, fnnlib is compared to other neural network libraries.
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.
Die Beschreibung des Verhaltens eines Multi-Agenten-Systems (MAS) ist eine fordernde Aufgabe, besonders dann, wenn es in sicherheitskritischen Umgebungen eingesetzt werden soll. Denn in solchen Umgebungen muss die Beschreibung besonders sorgfältig ausgeführt werden um Seiteneffekte zu vermeiden, die ungewünschte oder sogar zerstörerische Folgen haben könnten. Deshalb sind formale Methoden nützlich, die auf mathematischen Modellen des zu entwerfenden Systems basieren. Sie erlauben es nicht nur das System formal auf verschiedenen Abstraktionsebenen zu spezifizieren, sondern auch seine Konsistenz noch vor der Implementierung zu verifizieren. Das Ziel der formalen Spezifikation ist eine präzise und eindeutige Beschreibung des Verhaltens des Multi-Agenten-Systems, während die Verifikation darauf abzielt, geforderte Eigenschaften dieses Systems zu beweisen. Üblicherweise wird das Verhalten eines Agenten als diskrete Änderung seines Zustands im Bezug auf externe oder interne Aktionen aufgefasst. Jedes mal, wenn eine Aktion auftritt, ändert sich der Zustand des Agenten. Deshalb sind Zustandsübergangsdiagramme bzw. endliche Automaten ein naheliegender Ansatz das Verhalten zu modellieren. Ein weiterer Vorteil einer solchen Beschreibung ist, dass sie sich für das sogenannte Model Checking eignet. Dabei handelt es sich um eine automatische Analysetechnik, die bestimmt, ob das Modell des Systems spezifizierten Eigenschaften genügt. Allerdings muss in realistischen, physikalischen Umgebungen neben dem diskreten auch das kontinuierliche Verhalten des Multi-Agenten-Systems betrachtet werden. Dabei könnte es sich beispielsweise um die Schussbewegung eines Fußballspieler-Agenten, den Prozess des Löschens durch einen Feuerwehr-Agenten oder jedes andere Verhalten handeln, das auf zeitlichen physikalischen Gesetzen basiert. Die üblichen Zustandsübergangsdiagramme sind nicht ausreichend, um diese beiden Verhaltensarten zu kombinieren. Hybride Automaten stellen jedoch eine elegante Lösung dar. Im Wesentlichen erweitern sie die üblichen Zustandsübergangsdiagramme durch Methoden, die sich mit kontinuierlichen Aktionen befassen. Die Zustandsübergänge modellieren weiterhin die diskreten Verhaltenswechsel, während Differentialgleichungen verwendet werden um das kontinuierliche Verhalten zu beschreiben. Besonders geeignet erscheinen Hybride Automaten, weil ihre formale Semantik die Verifikation durch Model Checking erlaubt. Deshalb ist das Hauptziel dieser Arbeit, Hybride Automaten für die Modellierung und die Verifikation des Verhaltens von Multi-Agenten-Systemen einzusetzen. Jedoch bringt ihr Einsatz mehrere Probleme mit sich, die betrachtet werden sollten. Zu diesen Problemfeldern zählen Komplexität, Modularität und die Aussagestärke der Modelle. Diese Arbeit befasst sich mit diesen Problemen und liefert mögliche Lösungen.
Diese Arbeit behandelt verschiedene Ansätze zur Ermittlung einer Heuristik, welche zur Bestimmung einer optimalen Konfiguration des Theorembeweisers E-KRHyper eingesetzt werden soll. Es wird erläutert, wie der Beweiser durch eine angepasste Voreinstellung optimiert werden kann und die erarbeiteten Ansätze zur Ermittlung dieser Voreinstellung werden vorgestellt. Anhand der erzielten Ergebnisse werden die Ansätze anschließend bewertet und für eines der vorgestellten Verfahren wird außerdem eine Idee zur Implementierung vorgestellt.
Knowledge compilation is a common technique for propositional logic knowledge bases. A given knowledge base is transformed into a normal form, for which queries can be answered efficiently. This precompilation step is expensive, but it only has to be performed once. We apply this technique to concepts defined in the Description Logic ALC. We introduce a normal form called linkless normal form for ALC concepts and discuss an efficient satisability test for concepts given in this normal form. Furthermore, we will show how to efficiently calculate uniform interpolants of precompiled concepts w.r.t. a given signature.
In einer Welt, die immer mehr durch den Einsatz von Technik geprägt wird, gewinnen Systeme, welche eigenständig Aufgaben in einem vorgegebenen Kontext übernehmen können, mehr und mehr an Bedeutung. Solche Systeme werden als autonome Systeme bezeichnet, die ein eigenständiges Verhalten und Interaktionen mit ihrer Umwelt und anderen Systemen beinhalten. Zu diesen Systemen zählen auch autonome mobile Roboter. Sie sind sozusagen intelligente Fahrzeuge, die ihnen übertragene Aufgaben ohne menschliche Unterstützung durchführen können. Um ihre Umwelt wahrzunehmen, mit ihr interagieren und in ihr navigieren zu können benötigen diese Systeme verschiedene Arten von Sensoren. Somit ist die Robotikforschung stark interdisziplinär. Diese Arbeit befasst sich ausschliesslich mit dem Bereich der Navigation, insbesondere mit der Positionsbestimmung, welche für eine gute Navigation die Grundlage bildet. Ein heutzutage häufig benutztes, weltweit verfügbares System zur Positionsbestimmung ist GPS. Ziel dieser Arbeit ist der Anschluss eines GPS-Moduls an einen Mikrocontroller und der Versuch die Positionsgenauigkeit lokal zu präzisieren, um so einem autonomen System die Möglichkeit zur eröffnen, Aufgaben, die eine höhere Genauigkeit erfordern, zu bewerkstelligen.
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 semantic web and model-driven engineering are changing the enterprise computing paradigm. By introducing technologies like ontologies, metadata and logic, the semantic web improves drastically how companies manage knowledge. In counterpart, model-driven engineering relies on the principle of using models to provide abstraction, enabling developers to concentrate on the system functionality rather than on technical platforms. The next enterprise computing era will rely on the synergy between both technologies. On the one side, ontology technologies organize system knowledge in conceptual domains according to its meaning. It addresses enterprise computing needs by identifying, abstracting and rationalizing commonalities, and checking for inconsistencies across system specifications. On the other side, model-driven engineering is closing the gap among business requirements, designs and executables by using domain-specific languages with custom-built syntax and semantics. In this scenario, the research question that arises is: What are the scientific and technical results around ontology technologies that can be used in model-driven engineering and vice versa? The objective is to analyze approaches available in the literature that involve both ontologies and model-driven engineering. Therefore, we conduct a literature review that resulted in a feature model for classifying state-of-the-art approaches. The results show that the usage of ontologies and model-driven engineering together have multiple purposes: validation, visual notation, expressiveness and interoperability. While approaches involving both paradigms exist, an integrated approach for UML class-based modeling and ontology modeling is lacking so far. Therefore, we investigate the techniques and languages for designing integrated models. The objective is to provide an approach to support the design of integrated solutions. Thus, we develop a conceptual framework involving the structure and the notations of a solution to represent and query software artifacts using a combination of ontologies and class-based modeling. As proof of concept, we have implemented our approach as a set of open source plug-ins -- the TwoUse Toolkit. The hypothesis is that a combination of both paradigms yields improvements in both fields, ontology engineering and model-driven engineering. For MDE, we investigate the impact of using features of the Web Ontology Language in software modeling. The results are patterns and guidelines for designing ontology-based information systems and for supporting software engineers in modeling software. The results include alternative ways of describing classes and objects and querying software models and metamodels. Applications show improvements on changeability and extensibility. In the ontology engineering domain, we investigate the application of techniques used in model-driven engineering to fill the abstraction gap between ontology specification languages and programming languages. The objective is to provide a model-driven platform for supporting activities in the ontology engineering life cycle. Therefore, we study the development of core ontologies in our department, namely the core ontology for multimedia (COMM) and the multimedia metadata ontology. The results are domain-specific languages that allow ontology engineers to abstract from implementation issues and concentrate on the ontology engineering task. It results in increasing productivity by filling the gap between domain models and source code.
Die Arbeit beschäftigt sich mit der für Router und Kleingeräte entwickelten Linux-Distribution OpenWrt. Im ersten Teil der Arbeit wird die Erstellung von Softwarepaketen für OpenWrt erläutert und eine Anzeige- und Konfigurationskomponente für die Dateien des Quagga RIP-Daemons für die Benutzeroberfläche LuCI erstellt. Im zweiten Teil wird der Aufbau eines Testnetzwerkes mit OpenWrt Routern dokumentiert, sowie die Anbindung an VNUML-virtualisierte Netzwerke.
Folksonomien sind Web 2.0 Plattformen, in denen Benutzer verschiedene Inhalte miteinander teilen können. Die Inhalte können mit Hilfe von Stichwörtern, den sogenannten Tags, kategorisiert und organisiert werden. Die verschiedenen Folksonomien unterstützen unterschiedliche Inhaltstypen wie zum Beispiel Webseiten (Delicious), Bilder (Flickr) oder Videos (YouTube). Aufgrund ihrer einfachen Benutzungsweise haben Folksonomien viele Millionen Benutzer. Die einfache Benutzungsweise führt aber auch zu einigen Problemen. Diese Doktorarbeit beschäftigt sich mit drei der wichtigsten Probleme und beschreibt Methoden, wie sie gelöst werden können. Das erste dieser Probleme tritt auf, wenn Benutzer die Folksonomien nach bestimmten Inhalten durchsuchen wollen. Häufig können dabei nicht alle relevanten Inhalte gefunden werden, da diesen relevante Stichwörter fehlen. Dementsprechend tritt das zweite Problem während der Vergabe von Stichwörtern auf. Manche Folksonomien, wie zum Beispiel Delicious, unterstützen ihre Benutzer dabei, indem sie ihnen mögliche Stichwörter empfehlen. Andere Folksonomien, wie zum Beispiel Flickr, bieten keine solche Unterstützung. Die Empfehlung von Stichwörtern hilft dem Benutzer dabei, Inhalte auf einfache Art und Weise mit den jeweils relevanten Stichwörtern zu versehen. Das dritte Problem besteht darin, dass weder Stichwörter noch Inhalte mit einer festen Semantik versehen sind und mehrdeutig sein können. Das Problem entsteht dadurch, dass die Benutzer die Stichwörter vollkommen frei rnverwenden können. Die automatische Identifizierung der Semantik von Stichwörtern und Inhalten hilft dabei, die dadurch entstehenden Probleme zu reduzieren. Diese Doktorarbeit stellt mehrere Methoden vor, wie verschiedene Quellen für semantische Informationen benutzt werden können, um die vorher genannten drei Probleme zu lösen. In dieser Doktorarbeit benutzen wir als Quellen Internetsuchmaschinen, soziale Netzwerke im Internet und die gemeinsamen Vorkommen von Stichwörtern in Folksonomien. Die Verwendung der verschiedenen Quellen reduziert den Aufwand bei der Erstellung von Systemen, die die vorher genannten Probleme lösen. Die vorgestellten Methoden wurden auf einem großen Datensatz evaluiert. Die erzielten Ergebnisse legen nahe, dass semantische Informationen bei der Lösung der Probleme helfen, die während der Suche von Inhalten, der Empfehlung von Stichwörtern als auch der automatischen Identifizierung der Semantik von Stichwörtern und Inhalten auftreten.
Location Provider
(2011)
In dieser Arbeit wurde gemäß den in Kapitel 1.3 definierten Anforderungen ein System entwickelt, um mobile und in der Rechenleistung beschränkte Geräte wie Mobiltelefone und PDAs sowohl im Freien als auch in geschlossenen Räumen verorten zu können. Der eingeschränkten Leistungsfähigkeit der Geräte wird durch die Umsetzung einer Client-Server Lösung Rechnung getragen, bei der der Client als Sensorträger dient, der Daten aus seiner Umgebung registriert und über ein Kommunikationsnetz zur weiteren Berechnung an einen Server überträgt. Die Datenübertragung ist als Webservice realisiert, der auf offenen Standards wie XML und SOAP basiert und leicht um weitere Funktionen erweitert werden kann.
An der Universität Koblenz wurde mit dem RMTI (RIP with Metric based Topology Investigation) eine Erweiterung zu RIP entwickelt, die das Counting-to-Infinity Problem beheben soll. Eine lauffähige Implementierung des RMTI Algorithmus, auf Basis des RIP Daemons der Quagga Software Routing Suite, liegt vor. Openwrt ist ein, auf Linux basierendes, quelloffenes Betriebssystem für Router, wie z.B. den WRT54G der Firma Linksys. Die Möglichkeiten der Konfiguration der Router mit Openwrt gehen weit über die der original Firmware hinaus. So können die Router mit Software aus dem Linux-Bereich erweitert werden. Ziel dieser Studienarbeit ist die Installation des RMTI Daemons in Openwrt auf den Linksys WRT54G Routern der AG Rechnernetze. Anschließend sollen typische Netzwerksituationen aufgebaut und das Verhalten der Router untersucht werden.
Improvements to the RMTI network routing daemon implementation and preparation of a public release
(2011)
Routing with Metric based Topology Investigation (RMTI) is an algorithm meant to extend distance-vector routing protocols. It is under research and development at the University of Koblenz-Landau since 1999 and currently implemented on top of the well-known Routing Information Protocol (RIP). Around midyear 2009, the latest implementation of RMTI included a lot of deprecated functionality. Because of this, the first goal of this thesis was the reduction of the codebase to a minimum. Beside a lot of reorganization and a general cleanup, this mainly involved the removal of some no longer needed modes as well as the separation of the formerly mandatory XTPeer test environment. During the second part, many test series were carried out in order to ensure the correctness of the latest RMTI implementation. A replacement for XTPeer was needed and several new ways of testing were explored. In conjunction with this thesis, the RMTI source code was finally released to the public under a free software license.
Towards Improving the Understanding of Image Semantics by Gaze-based Tag-to-Region Assignments
(2011)
Eye-trackers have been used in the past to identify visual foci in images, find task-related image regions, or localize affective regions in images. However, they have not been used for identifying specific objects in images. In this paper, we investigate whether it is possible to assign image regions showing specific objects with tags describing these objects by analyzing the users' gaze paths. To this end, we have conducted an experiment with 20 subjects viewing 50 image-tag-pairs each. We have compared the tag-to-region assignments for nine existing and four new fixation measures. In addition, we have investigated the impact of extending region boundaries, weighting small image regions, and the number of subjects viewing the images. The paper shows that a tag-to-region assignment with an accuracy of 67% can be achieved by using gaze information. In addition, we show that multiple regions on the same image can be differentiated with an accuracy of 38%.
Die modellgetriebene Softwareentwicklung beabsichtigt die Spezifikation von Softwaresystemen durch Modelle zu vereinfachen und die automatisierte Entwicklung zu verbessern. Die Modellierungssprachen und Werkzeuge, die zur Modellierung von Systemen und Anwendungsdomänen herangezogen werden, werden in modellbasierten technologischen Räumen zusammengefasst. Ontologiebasierte technologische Räume enthalten Ontologiesprachen und Technologien zum Entwurf, der Anfrage und dem Schlussfolgern von Wissen. Mit der Verbreitung des semantischen Webs werden Ontologien in der Entwicklung von Software zunehmend eingesetzt.
In dieser Arbeit werden zur Kombination von technologischen Räumen Brückentechnologien vorgestellt. Transformationsbrücken übersetzen Modelle, Abbildungsbrücken stellen Beziehungen zwischen Modellen verschiedener technologischer Räume her und Integrationsbrücken verschmelzen Räume zu neuen allumfassenden technologischen Räumen. API Brücken erschaffen Interoperabilität zwischen Werkzeugen. Diese Arbeit beschäftigt sich insbesondere mit der Kombination von modellbasierten und ontologiebasierten technologischen Räumen. Nach einem Vergleich zwischen Sprachen und Werkzeugen der einzelnen Räume wird die Integrationsbrücke herangezogen um einen neuen gemeinsamen technologischen Raum zu erstellen, der den hybriden Gebrauch von Sprachen und den interoperablen Einsatz von Werkzeugen ermöglicht. Die Syntax und Semantik von Modellierungssprachen kann mit Hilfe von Ontologiesprachen spezifiziert werden. Die Korrektheit von Modellen wird durch den Einsatz von Ontologietechnologien gewährleistet. Ontologiebasierte Modellierungssprachen erlauben den Nutzen von Anfrage- und Schlussfolgerungstechnologien. Sie sind darüber hinaus so flexibel um verschiedene Anforderungen von Softwareentwicklern zu erfüllen. Domänenspezifische Sprachen unterstützen neben der Spezifikation von Systemen auch die konzeptionelle Beschreibung von Domänen durch Modelle, die aus möglichen Laufzeitinstanzen und deren Typen bestehen. Integrierte Ontologiesprachen helfen eine formale Semantik für Domänenmodellierungssprachen zu definieren und Ontologietechnologien ermöglichen das Schlussfolgern über Typen und Instanzen.
Alle Ansätze in dieser Arbeit werden mit Hilfe eines Szenarios, in dem die Konfigurationen für Familien von Netzwerkgeräte modelliert werden, veranschaulicht. Ferner werden die Implementationen aller Brückentechnologien zur Kombination von technologischen Räumen und alle Werkzeuge für die ontologiebasierte Entwicklung von Modellierungssprachen illustriert.
Die vorliegende Dissertation untersucht die Entstehung von Dialekten innerhalb des in dieser Arbeit entworfenen Modells einer Multi-Agenten-Simulation, basierend auf neuronalen Netzen. Zunächst werden die linguistischen Grundlagen detailliert dargestellt. Dazu gehört neben der Diskussion einiger Definitionen von Sprache ein Überblick über die sprachlichen Evolutionsstufen, eine Übersicht der Bestandteile menschlicher Hochsprachen mitsamt den bekannten Möglichkeiten ihrer Veränderung und eine Übersicht tierischer Sprachen mit kommunikativer Funktion und ihrer Dialektbildung.
Im Anschluss werden die Grundlagen der Informatik und Mathematik erläutert. Diese umfassen neben den Begriffen Modell und Simulation den Aufbau einer Multi-Agenten-Simulation und die Funktionsweise künstlicher neuronaler Netze. Aus den hier genannten Grundlagen wird daraufhin ausführlich das Simulationsmodell dieser Arbeit hergeleitet und beschrieben.
Die Ergebnisse vieler hundert verschiedener Simulationsdurchläufe werden im Anschluss erläutert. So werden die im Modell definierten Störfaktoren einzeln untersucht und in Werteintervalle mit unterschiedlichen Auswirkungen eingeteilt. Weiterhin werden vorhandene Wechselwirkungen der Faktoren aufgezeigt und der Prozess der Sprachwiedervereinigung nach einer vorherigen Dialektspaltung gezeigt.
Einem Fazit und Ausblick folgen als Anhänge Anforderungsdefinition, Entwurf, Architektur, eine detaillierte Erläuterung der Implementierung und ein englischsprachiges Benutzerhandbuch des Werkzeugs DiaLex. DiaLex ist ein komplett in Java konzipiertes und implementiertes Programm und bietet dem Benutzer die Möglichkeit, den Einfluss verschiedener Störfaktoren auf die Dialektbildung innerhalb einer gemeinsam genutzten Sprache einer oder mehrerer Agentengemeinschaften zu simulieren und zu analysieren.
Die Arbeit entstand im Zeitraum Oktober 2007 bis Juni 2010 an der Universität Koblenz-Landau.
Nagios unter VNUML
(2011)
This paper documents the development of an abstract physics layer (APL) for Simspark. After short introductions to physics engines and Simspark, reasons why an APL was developed are explained. The biggest part of this paper describes the new design and why certain design choices were made based on requirements that arose during developement. It concludes by explaining how the new design was eventually implemented and what future possibilities the new design holds.
Der immer schnellere technologische Wandel in der Wirtschaft und die damit verbundenen, sich verkürzenden Innovationszyklen machen die Aus- und Weiterbildung der Mitarbeitenden eines Unternehmens zu einem wichtigen Wettbewerbsfaktor. Traditionelle (Weiter-)Bildungsmethoden können jedoch den resultierenden, ständig wachsenden und immer schneller zu befriedigenden Aus- und Weiterbildungsbedarf nur bedingt befriedigen. Deshalb werden in zunehmenden Maße in der Aus- und Weiterbildung Angebote aus dem Bereich des technologiebasierten Lernens eingesetzt, welche ein selbstgesteuertes und -organisiertes Lernen und durch eine Integration in tägliche Arbeitsabläufe einen optimalen Wissenstransfer mit entsprechend hohem Lernerfolg ermöglichen. Um dies aber auch zu realisieren, ist eine entsprechend hohe Angebotsqualität in Bezug auf die Unterstützung der Nutzenden bei der Erreichung ihrer Lernziele erforderlich. Die Entwicklung qualitativ hochwertiger technologiebasierter Lernangebote ist im Allgemeinen aber mit größeren Aufwänden und längeren Entwicklungszeiten verbunden, wodurch eine Verfügbarkeit eines solchen Angebots zeitnah zum entstandenen Bedarf und in der geforderten Qualität oftmals nicht gewährleistet werden kann.
Diese Arbeit beschäftigt sich deshalb mit der Forschungsfrage, wie eine Lernsoftware entwickelt werden muss, um eine qualitativ hochwertige LSW im Sinne der optimalen Ausrichtung auf die Eigenschaften und Lernziele der einzelnen Lernenden sowie auf den von ihnen geplanten Einsatzkontext für das vermittelte Wissen bei gleichzeitiger Reduzierung von Entwicklungsaufwand und -zeit zu produzieren. Die als Antwort auf die Forschungsfrage definierte IntView-Methodik zur systematischen, effizienten und zeitnahen Entwicklung von qualitativ hochwertigen technologiebasierten Lernangeboten wurde konzipiert, um die Wahrscheinlichkeit der Produktion der Angebote ohne Überschreitung von Projektzeitplänen und -budgets bei gleichzeitiger gezielter Ausrichtung des Angebots auf Zielgruppen und Einsatzkontexte zur Gewährleistung der Qualität zu erhöhen.
Hierzu wurden nach einer umfangreichen Untersuchung von bestehenden Ansätzen zur Lernsoftware-Entwicklung, aber auch zur Produktion von verwandten Produkten wie Multimedia-, Web- oder Software-Anwendungen, diejenigen Durchführungsvarianten der Aktivitäten bzw. Aktivitätsschritte zur Lernsoftware-Entwicklung zu einer systematischen Vorgehensweise integriert, welche in ihrem Zusammenspiel den größten Beitrag zu einer effizienten Produktion leisten können. Kern der Methodik ist ein Entwicklungsprozess zur ingenieursmäßigen Erstellung der Angebote, der alle Entwicklungsphasen abdeckt und die Vorgehensweisen und Methoden aller an der Entwicklung beteiligten Fachdisziplinen, inklusive einer kontinuierlichen Qualitätssicherung von Projektbeginn an, in einen gemeinsamen Prozess integriert. Dieser Prozess wird sowohl als Lebenszyklusmodell als auch als daraus abgeleitetes Prozessmodell in Form eines Abhängigkeitsmodells definiert, um eine optimale Unterstützung eines Projektteams bei Koordination und Abstimmung der Arbeiten in der Entwicklung zu ermöglichen. In Ergänzung zu den Modellen wird eine umfassende Arbeitsunterstützung mit Templates bzw. Dokumentvorlagen inklusive Handlungsanweisungen und Beispielen für die direkte Anwendung der Vorgehensweise durch die Nutzenden bereit gestellt.
Im Rahmen der Evaluation der Methodik wird der Nachweis geführt, dass sie im Zusammenspiel mit ihrer umfangreichen Autorenunterstützung eine sowohl effektive als auch effiziente Lernangebot-Entwicklung ermöglichen kann. In den hierfür durchgeführten Beispielprojekten als auch in den durchgeführten drei Fallstudien wird gezeigt, dass die Methodik zum einen an die Erstellung unterschiedlicher Arten von Lernangeboten bzw. an den Einsatz in verschiedenen Projektkontexten einfach anpassbar sowie zum anderen effizient und effektiv nutzbar ist.
Modern Internet and Intranet techniques, such as Web services and virtualization, facilitate the distributed processing of data providing improved flexibility. The gain in flexibility also incurs disadvantages. Integrated workflows forward and distribute data between departments and across organizations. The data may be affected by privacy laws, contracts, or intellectual property rights. Under such circumstances of flexible cooperations between organizations, accounting for the processing of data and restricting actions performed on the data may be legally and contractually required. In the Internet and Intranet, monitoring mechanisms provide means for observing and auditing the processing of data, while policy languages constitute a mechanism for specifying restrictions and obligations.
In this thesis, we present our contributions to these fields by providing improvements for auditing and restricting the data processing in distributed environments. We define formal qualities of auditing methods used in distributed environments. Based on these qualities, we provide a novel monitoring solution supporting a data-centric view on the distributed data processing. We present a solution for provenance-aware policies and a formal specification of obligations offering a procedure to decide whether obligatory processing steps can be met in the future.
The paper deals with a specific introduction into probability propagation nets. Starting from dependency nets (which in a way can be considered the maximum information which follows from the directed graph structure of Bayesian networks), the probability propagation nets are constructed by joining a dependency net and (a slightly adapted version of) its dual net. Probability propagation nets are the Petri net version of Bayesian networks. In contrast to Bayesian networks, Petri nets are transparent and easy to operate. The high degree of transparency is due to the fact that every state in a process is visible as a marking of the Petri net. The convenient operability consists in the fact that there is no algorithm apart from the firing rule of Petri net transitions. Besides the structural importance of the Petri net duality there is a semantic matter; common sense in the form of probabilities and evidencebased likelihoods are dual to each other.
Dualizing marked Petri nets results in tokens for transitions (t-tokens). A marked transition can strictly not be enabled, even if there are sufficient "enabling" tokens (p-tokens) on its input places. On the other hand, t-tokens can be moved by the firing of places. This permits flows of t-tokens which describe sequences of non-events. Their benefiit to simulation is the possibility to model (and observe) causes and effects of non-events, e.g. if something is broken down.
In this paper, we demonstrate by means of two examples how to work with probability propagation nets (PPNs). The fiirst, which comes from the book by Peng and Reggia [1], is a small example of medical diagnosis. The second one comes from [2]. It is an example of operational risk and is to show how the evidence flow in PPNs gives hints to reduce high losses. In terms of Bayesian networks, both examples contain cycles which are resolved by the conditioning technique [3].
Cheops für VNUML - Erstellen und beobachten einer VNUML-Simulation per MausklickrnEs wird untersucht, wie Virtual Network User Mode Linux (VNUML), eine Software zur Simulation von Rechnernetzen, die aus virtualisierten Linux Instanzen aufgebaut werden, für den Benutzer besser handhabbar gemacht werden kann. Mit dem Linux-Paket VNUML, welches die dateigesteuerte Konfiguration virtueller Betriebssysteminstanzen ermöglicht, erhält der Anwender die Möglichkeit, komplexe Netzwerktopologien zu simulieren. Verschiedene Netzwerküberwachungsprogramme werden auf ihre Fähigkeit hin untersucht, eine laufende VNUML-Simulation zu erfassen und sinnvoll abzubilden. Dabei soll der Benutzer einen schnellen Überblick über die Funktion der simulierten Netzwerkumgebung, sowie nach Möglichkeit auch über deren Topologie erhalten können. Das Programm Cheops, welches der Netzwerküberwachung dient, wird erweitert, um nicht nur eine laufende Simulation abbilden und beobachten zu können, sondern darüber hinaus in der Lage zu sein, in jedem Schritt der Arbeit mit VNUML eingesetzt zu werden.
Das erweiterte Programm gestattet sowohl die Erstellung der VNUML-Topologiedatei, als auch das Starten und Steuern der Simulation. Damit werden der lange Kommandozeilenaufruf, sowie das Editieren der Konfigurationsdatei, durch einfach zu benutzende Funktionen in einer grafischen Oberfläche (GUI) ersetzt. Zur schnellen Kontrolle der vollen Funktionsfähigkeit der gestarteten Simulation sind keine weiteren Eingaben oder Konfigurationen nötig. Ebenso kann eine differenzierte Beobachtung verschiedener Netzwerkdienste während der Laufzeit der Simulation erfolgen. Die hierzu nötigen Werkzeuge sind im Paket Cheops für VNUML ebenfalls enthalten und speziell zur Anwendung mit VNUML-Simulationen vorkonfiguriert.
Die vorliegende Dissertation behandelt den Einsatz von Theorembeweise innerhalb der automatischen Fragebeantwortung (question answering - QA). QA-Systeme versuchen, natürlichsprachliche Fragen korrekt zu beantworten. Sie verwenden eine Vielzahl von Methoden aus der Computerlinguistik und der Wissensrepräsentation, um menschliche Sprache zu verarbeiten und die Antworten aus umfangreichen Wissensbasen zu beziehen. Diese Methoden sind allerdings meist syntaxbasiert und können kein implizites Wissen herleiten. Die Theorembeweiser der automatischen Deduktion dagegen können Folgerungsketten mit Millionen von Inferenzschritten durchführen. Die Integration eines Beweisers in ein QA-System eröffnet die Möglichkeit, aus den Fakten einer Wissensbasis neues Wissen herzuleiten und somit die Fragebeantwortung zu verbessern. Herausforderungen liegen in der Überwindung der gegensätzlichen Herangehensweisen von Fragebeantwortung und Deduktion: Während QA-Methoden normalerweise darauf abzielen, auch mit unvollständigen oder fehlerhaften Daten robust und schnell zu halbwegs annehmbaren Ergebnissen zu kommen, verwenden Theorembeweiser logische Kalküle zur Gewinnung exakter und beweisbarer Resultate. Letzterer Ansatz erweist sich sich aber als schwer vereinbar mit der Quantität und der Qualität der im QA-Bereich üblichen Wissensbestände.
Die Dissertation beschreibt Anpassungen von Theorembeweisern zur Überwindung dieser Hürden. Zentrales Beispiel ist der an der Universität Koblenz-Landau entwickelte Beweiser E-KRHyper, der im Rahmen dieser Dissertation in das QA-System LogAnswer integriert worden ist. Außerdem vorgestellt werden zusätzliche Erweiterungsmöglichkeiten auf der Implementierungs- und der Kalkülebene, die sich aus dem praktischen Einsatz bei der Fragebeantwortung ergeben haben, dabei aber generell für Theorembeweiser von Nutzen sein können. Über die reine Deduktionsverbesserung der QA hinausgehend beinhalten diese Erweiterungen auch die Anbindung externer Wissensquellen wie etwa Webdienste, mit denen der Beweiser während des Deduktionsvorgangs gezielt Wissenslücken schließen kann. Zudem ermöglicht dies die Nutzung externer Ontologien beispielsweise zur Abduktion. Evaluationsergebnisse aus eigenen Versuchsreihen und aus Wettbewerben demonstrieren die Effektivität der diskutierten Methoden.
Interaktive Visualisierungen für den Linking- und Suchprozess heterogener Informationen im Web
(2013)
Die Informationsmenge im Web nimmt stetig zu und auch die Art und Vielfalt von Informationen wird immer größer. Es stehen die unterschiedlichsten Informationen wie Nachrichten, Artikel, Statistiken, Umfragedaten, Börsendaten, Veranstaltungen, Literaturnachweise usw. zur Verfügung. Die Informationen zeichnen sich durch Heterogenität in Aspekten wie Informationsart, Modalität, Strukturiertheit, Granularität, Qualität und ihre Verteiltheit aus. Die zwei Haupttechniken, mit denen Nutzer im Web nach diesen Informationen suchen, sind die Suche mit Websuchmaschinen und das Browsing über Links zwischen Informationseinheiten. Die vorherrschende Art der Informationsdarstellung ist dabei weitgehend statisch in Form von Text, Bildern und Grafiken. Interaktive Visualisierungen bieten eine Reihe von Vorteilen für die Aufbereitung und Exploration von heterogenen Informationen im Web: (1) Sie bieten verschiedene Darstellungsformen für unterschiedliche, sehr große und auch komplexe Informationsarten und (2) große Datenmengen können interaktiv anhand ihrer Eigenschaften exploriert werden und damit den Denkprozess des Nutzers unterstützen und erweitern. Bisher sind interaktive Visualisierungen aber noch kein integraler Bestandteil des Suchprozesses im Web. Die technischen Standards und Interaktionsparadigmen, um interaktive Visualisierungen als Massentechnik im Web nutzbar zu machen, werden erst langsam durch Standardisierungsgremien eingeführt. Diese Arbeit untersucht, wie interaktive Visualisierungen für den Linking- und Suchprozess heterogener Informationen im Web eingesetzt werden können. Basierend auf Grundlagen in den Bereichen Informationssuche, Informationsvisualisierung und Informationsverarbeitung wird ein Modell gebildet, das bestehende Strukturmodelle der Informationsvisualisierung um zwei neue Prozesse erweitert: (1) das Linking von Informationen in Visualisierungen und (2) das Glyphenbasierte Suchen, Browsen und Filtern. Das Vizgr-Toolkit implementiert das entwickelte Modell in einer Webanwendung. In vier verschiedenen Anwendungsszenarien werden Teilaspekte des Modells instanziiert und in Nutzertests evaluiert oder anhand von Beispielen untersucht.
E-KRHyper is a versatile theorem prover and model generator for firstorder logic that natively supports equality. Inequality of constants, however, has to be given by explicitly adding facts. As the amount of these facts grows quadratically in the number of these distinct constants, the knowledge base is blown up. This makes it harder for a human reader to focus on the actual problem, and impairs the reasoning process. We extend E-Hyper- underlying E-KRhyper tableau calculus to avoid this blow-up by implementing a native handling for inequality of constants. This is done by introducing the unique name assumption for a subset of the constants (the so called distinct object identifiers). The obtained calculus is shown to be sound and complete and is implemented into the E-KRHyper system. Synthetic benchmarks, situated in the theory of arrays, are used to back up the benefits of the new calculus.
In dieser Studienarbeit sollen verschiedene Routing-Lookup Algorithmen aufgelistet und verglichen werden, mit denen eine Routing-Tabelle erstellt und angepasst werden kann. Dazu werden hier nur dynamische Verfahren in Betracht gezogen. Allgemein wird die Funktionsweise einer Routing-Tabelle erklärt und drei Verfahren bzw. Algorithmen analysiert und bewertet. Die Algorithmen werden anhand von Beispielen erläutert und in einem abschließenden Kapitel gegenüber gestellt. Dabei werden die Vor- und Nachteile der einzelnen Verfahren aufgelistet.
The Apple ][ computer was one of the frst three completely assembled systems on the market. It was sold several million times from april 1977 to 1993. This 8 bit home computer was developed by Steve Wozniak and Steve Jobs. They paved the way for the Apple Macintosh computer and the nowadays well known brand Apple with its products.
This thesis describes the implementation of a software emulator for the complete Apple ][ computer system on a single Atmel AVR microcontroller unit (MCU). The greatest challenge consists of the fact that the MCU has only a slightly higher clock speed as the Apple ][. This requires an efcient emulation of the CPU and the memory management, which will be covered later on along with the runtime environment controlling the emulator. Furthermore the hardware implementation into a handheld prototype will be shown.
In summary this thesis presents a successful development of a portable Apple ][ emulator covering all aspects from software design over hardware design ending up in a prototype.
In diesem Bericht wird der Einsatz von drahtlosen Sensornetzen zur Temperaturmessung in Fließgewässern untersucht. Es wird dargestellt, inwieweit solche Netze als Bindeglied zwischen Fernerkundung und stationären Sensoren eingesetzt werden können. Es werden die Anforderungen an Sensornetze für die Anwendung Gewässermonitoring ermittelt und eine prototypische Realisierung von Netzknoten für ein solches Sensornetz dargestellt. Als Ergebnis dieser Arbeit werden die Genauigkeit von Temperaturmessungen mit solchen Sensorknoten im Vergleich zu einem Temperaturlogger als Referenzsystem dargestellt. Die Messungen zeigen, dass eine vergleichsweise gute Messgenauigkeit zu geringen Kosten erreichbar ist. Durch Weiterentwicklung des hier dargestellten Prototypen steht für die Temperaturüberwachung in Gewässern ein vielversprechendes und kostengünstiges neues Messinstrument zur Verfügung. Dieses kann auf der einen Seite in tieferen Regionen Gewässertemperaturen messen, als dies mit Fernerkundung möglich ist, und auf der anderen Seite eine höhere räumliche Auflösung als stationäre Messstationen erreichen. Zusätzlich dienen die Literaturrecherche und die Formulierung der Kriterien einer Eingrenzung des Anwendungsbereichs für weiterführende Arbeiten.
Die Diffusionsbildgebung misst die Bewegung von Wassermolekülen in Gewebe mittelsrnvariierender Gradientenfelder unter Verwendung der Magnetresonanztomographie(MRT). Diese Aufnahmetechnik stellt eine große Chance für in vivo Untersuchung von neuronalen Bahnen dar, da das lokale Diffusionsprofil Rückschlüsse über die Position und Richtung von Nervenbahnen erlaubt. Zu den Anwendungsgebieten der Diffusionsbildgebung zählt die Grundlagenforschung in den Neurowissenschaften, in denen Nervenbahnen als Verbindungen kortikaler Areale bestimmt werden, und die neurochirurgische Operationsplanung, in der rekonstruierte Bahnen als Risikostrukturen für Interventionen angesehen werden.
Die Diffusionstensor-MRT (DT-MRT) ist aufgrund ihrer schnellen Aufnahme- und Rekonstruktionsgeschwindigkeit derzeitig klinischer Standard zur Bestimmung von Nervenbahnen. Jedoch erlaubt die DT-MRT nicht die Darstellung von komplexen intravoxel Diffusionsverteilungen. Daher etablierte sich eine weitere Modellierungstechnik, die als High Angular Resolution Diffusion Imaging (HARDI) bekannt ist. HARDITechniken erhielten wachsendes Interesse in den Neurowissenschaften, da sie großes Potential zur exakteren Darstellung der Nervenbahnen im menschlichen Gehirn besitzen.
Um die Vorteile von HARDI-Techniken gegenüber DT-MRT voll auszuschöpfen, werden fortgeschrittene Methoden zur Rekonstruktion und Visualisierung der Bahnen benötigt. In der vorliegenden Arbeit werden neue Techniken vorgestellt, welche zur aktuellen Forschung hinsichtlich der Verarbeitung und Visualisierung von Diffusionsbildgebungsdaten beitragen. Ansätze zur Klassifizierung, Traktographie und Visualisierung wurden entwickelt um eine aussagekräftige Exploration neuronaler Bahnen und deren Beschaffenheit zu ermöglichen. Des Weiteren wurde eine interaktive Software für die neurochirurgische Operationsplanung implementiert, welche Nervenbahnen als Risikostrukturen berücksichtigt.
Die vorgestellten Forschungsergebnisse bieten einen erweiterten und aufgabenorientierten Einblick in neuronale Verbindungen sowohl für Neurowissenschaftler als auch für Neurochirurgen und tragen zum Einsatz von HARDI-Techniken in einer klinischen Umgebung bei.
Diese Bachelorarbeit befasst sich mit der Entwicklung und Implementierung einer Gesichtserkennenden Software, die in der Lage ist Personenströme zurnerkennen und zu protokollieren. Dabei wird, ausgehend von den speziellen Anforderungen der Bildverarbeitung die entstandene Softwarearchitektur und deren Implementation vorgestellt. Zusätzlich wird zur Implementation ein Webinterface entwickelt welches die Verwaltung der Daten vereinfachen soll. Abschließend werden weitere Verfahren der Gesichtserkennung vorgestellt und gegen das eingesetzte Verfahren verglichen. Zum Schluss wird die implementierte Software evaluiert.
In den letzten Jahren gibt es im Bereich Software Engineering ein steigendes Interesse an empirischen Studien. Solche Studien stützen sich häufig auf empirische Daten aus Corpora-Sammlungen von Software-Artefakten. Während es etablierte Formen der Durchführung solcher Studien gibt, wie z.B. Experimente, Fallstudien und Umfragen, geschieht die Vorbereitung der zugrunde liegenden Sammlung von Software-Artefakten in der Regel ad hoc.
In der vorliegenden Arbeit wird mittels einer Literaturrecherche gezeigt, wie häufig die Forschung im Bereich Software Engineering Software Corpora benutzt. Es wird ein Klassifikationsschema entwickelt, um Eigenschaften von Corpora zu beschreiben und zu diskutieren. Es wird auch erstmals eine Methode des Corpus (Re-)Engineering entwickelt und auf eine bestehende Sammlung von Java-Projekten angewendet.
Die Arbeit legt zwei umfassende empirische Studien vor, in denen eine umfangreiche und breit angelegte Analysenreihe zu den Sprachen Privacy Preferences (P3P) und objektorientierte Programmierschnittstellen (APIs) durchgeführt wird. Beide Studien stützen sich allein auf die vorliegenden Daten der Corpora und decken dadurch die tatsächliche Nutzung der Sprachen auf.