Filtern
Erscheinungsjahr
Dokumenttyp
- Ausgabe (Heft) zu einer Zeitschrift (36)
- Dissertation (29)
- Masterarbeit (8)
- Diplomarbeit (4)
- Studienarbeit (4)
- Bachelorarbeit (2)
Sprache
- Englisch (83) (entfernen)
Schlagworte
- Bluetooth (4)
- Software Engineering (4)
- Knowledge Compilation (3)
- Semantic Web (3)
- Campus Information System (2)
- E-KRHyper (2)
- Equality (2)
- Modellgetriebene Entwicklung (2)
- Ontology (2)
- Petri-Netze (2)
Institut
- Institut für Informatik (83) (entfernen)
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.