004 Datenverarbeitung; Informatik
Filtern
Erscheinungsjahr
Dokumenttyp
- Dissertation (48) (entfernen)
Schlagworte
- Software Engineering (4)
- Information Retrieval (3)
- model-based (3)
- Abduktion <Logik> (2)
- Maschinelles Lernen (2)
- Modellgetriebene Entwicklung (2)
- Petri-Netz (2)
- Visualisierung (2)
- 3D Modell Referenz Bildsynthese (1)
- AUTOSAR (1)
Tagging-Systeme sind faszinierende dynamische Systeme in denen Benutzer kollaborativ Ressourcen mit sogenannten Tags indexieren. Um das volle Potential von Tagging-Systemen nutzen zu können ist es wichtig zu verstehen, wie sich das Verhalten der einzelnen Benutzer auf die Eigenschaften des Gesamtsystems auswirkt. In der vorliegenden Arbeit wird das Epistemic Dynamic Model präsentiert. Es schlägt eine Brücke zwischen dem Benutzerverhalten und den Systemeigenschaften. Das Modell basiert auf der Annahme, dass der Einfluss des gemeinsamen Hintergrundwissens der Benutzer und der Imitation von Tag-Vorschlägen ausreicht, um die Entstehung der Häufigkeitsverteilungen der Tags und des Wachstums des Vokabulars zu erklären. Diese beiden Eigenschaften eines Tagging-Systems hängen eng mit der Entstehung eines gemeinsamen Vokabulars der Benutzer zusammen. Mit Hilfe des Epistemic Dynamic Models zeigen wir, dass die generelle Ausprägung der Tag-Häufigkeitsverteilungen und des Wachstums des Vokabulars ihren Ursprung in dem gemeinsamen Hintergrundwissen der Benutzer haben. Tag-Vorschläge können dann dazu genutzt werden, um gezielt diese generelle Ausprägung zu beeinflussen. In der vorliegenden Arbeit untersuchen wir hauptsächlich den Einfluss der von Vorschlägen populärer Tags ausgeht. Populäre Tags sorgen für einen Feedback-Mechanismus zwischen den Vokabularen der einzelnen Benutzer, der die Inter-Indexer Konsistenz der Tag-Zuweisungen erhöht. Wie wird aber dadurch die Indexierungsqualität in Tagging-Systemen beeinflusst? Zur Klärung dieser Frage untersuchen wir eine Methode zur Messung der Inter-Ressourcen Konsistenz der Tag-Zuweisungen. Die Inter-Ressourcen Konsistenz korreliert positiv mit der Indexierungsqualität, und mit der Trefferquote und der Genauigkeit von Suchanfragen an das System. Sie misst inwieweit die Tag-Vektoren die durch Benutzer wahrgenommene Ähnlichkeit der jeweiligen Ressourcen widerspiegeln. Wir legen mit Hilfe unseres Modell dar, und zeigen es auch mit Hilfe eines Benutzerexperiments, dass populäre Tags zu einer verringerten Inter-Ressourcen Konsistenz führen. Des Weiteren zeigen wir, dass die Inter-Ressourcen Konsistenz erhöht wird, wenn dem Benutzer das eigene, bisher genutzte Vokabular vorgeschlagen wird. Unsere Methode zur Messung der Inter-Ressourcen Konsistenz ergänzt bestehende Evaluationsmaße für Tag-Vorschlags-Algorithmen um den Aspekt der Indexierungsqualität.
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.
In dieser Doktorarbeit beschreibe ich das spektrale Verhalten von großen, dynamischen Netzwerken und formuliere das spektrale Evolutionsmodell. Das spektrale Evolutionsmodell beschreibt das Wachstum von Netzwerken, die sich im Laufe der Zeit ändern, und charakterisiert ihre Eigenwert-und Singulärwertzerlegung. Das spektrale Evolutionsmodell sagt aus, dass im Laufe der Zeit die Eigenwerte eines Netzwerks wachsen, und die Eigenvektoren nahezu konstant bleiben. Ich validiere das spektrale Evolutionsmodell empirisch mit Hilfe von über einhundert Netzwerkdatensätzen, und theoretisch indem ich zeige,dass es eine gewisse Anzahl von bekannten Algorithmen zur Kantenvorhersage verallgemeinert, darunter Graph-Kernel, Pfad-Zähl-Methoden, Rangreduktion und Triangle-Closing.
Die Sammlung von Datensätzen, die ich verwende enthält 118 distinkte Datensätze. Ein Datensatz, das soziale Netzwerk mit negativen Kanten des Slashdot-Zoo, wurde speziell während des Verfassens dieser Arbeit extrahiert. Ich zeige auch, dass das spektrale Evolutionsmodell als Generalisierung des Preferential-Attachment-Modells verstanden werden kann, wenn Wachstum in latenten Dimensionen einzeln betrachtet wird. Als Anwendungen des spektralen Evolutionsmodells führe ich zwei neue Algorithmen zur Kantenvorhersage ein, die in Empfehlungssystemen, Suchmaschinen, im Collaborative-Filtering, für die Vorhersage von Bewertungen, für die Vorhersage von Kantenvorzeichen und mehr verwendet werden können. Der erste Kantenvorhersagealgorithmus ergibt ein eindimensionales Curve-Fitting-Problem, aus dem eine spektrale Transformation gelernt wird. Die zweite Methode verwendet Extrapolation von Eigenwerten, um zukünftige Eigenwerte vorherzusagen. Als Spezialfälle zeige ich, dass das spektrale Evolutionsmodell auf gerichtete, ungerichtete, gewichtete, ungewichtete, vorzeichenbehaftete und bipartite Graphen erweitert werden kann. Für vorzeichenbehaftete Graphen führe ich neue Anwendungen der Laplace-Matrix zur Graphzeichnung, zur spektralen Clusteranalyse, und beschreibe neue Laplace-Graph-Kernel, die auf vorzeichenbehaftete Graphen angewendet werden können.
Ich definiere dazu den algebraischen Konflikt, ein Maß für den Konflikt, der in einem vorzeichenbehafteten Graphen vorhanden ist, und das auf der vorzeichenbehafteten Laplace-Matrix begründet ist. Ich beschreibe das Problem der Vorhersage von Kantenvorzeichen spektral, und führe die vorzeichenbehaftete Widerstands-Distanz ein. Für bipartite und gerichtete Graphen führe ich den Sinus-Hyperbolicus-und ungeraden Neumann-Kernel ein, welche den Exponential- und den Neumann-Kernel für ungerichtete unipartite Graphen verallgemeinern. Ich zeige zudem, dass das Problem der gerichteten und bipartiten Kantenvorhersage verwandt sind, dadurch dass beide durch die Evolution der Singulärwertzerlegung gelöst werden können.
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.
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.
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 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.
Moderne Instant-Messaging-Systeme als Plattform für sicherheitskritische kollaborative Anwendungen
(2010)
Während unter dem Begriff Instant Messaging (IM) ursprünglich nur der Austausch von Textnachrichten (Messaging, Chat) verstanden wurde, bieten heutige Instant-Messaging-Systeme (IM-Systeme, IMS) darüber hinaus viele weitere Funktionen wie Sprachtelefonie, Videokonferenz oder Dateiübertragung an. Aktuelle IM-Systeme werden vor allem in der privaten unverbindlichen Kommunikation eingesetzt. Diese Systeme eignen sich " wie in dieser Arbeit gezeigt wird " aber auch für den Einsatz im geschäftlichen Kontext. Zu den Vorzügen, die sich aus der Nutzung eines IM-Systems ergeben, gehören beispielsweise die spontane, flexible und kostengünstige Nutzung unabhängig von Ort und Zeit, die einfache Verteilung von Informationen an mehrere Teilnehmer und die Verfügbarkeit verschiedener Kommunikationskanäle für unterschiedliche Aufgaben. Der Ursprung dieser Systeme (kurzer informeller Nachrichtenaustausch), ihr modularer Aufbau, die unkontrollierte Installation auf Clients sowie der daraus entstehende Informationsfluss führten zu zahlreichen Fragen und Herausforderungen bezüglich ihrer Sicherheit. So kann beispielsweise nicht ohne weiteres kontrolliert werden, welche Informationen ein Unternehmen auf diesem Weg verlassen. Anders als bei anderen elektronischen Kommunikationsmedien (E-Mail, Web) sind hier noch keine bekannten Sicherheitsmechanismen etabliert (z. B. Spam-Filter, Sicherheitsfunktionen von Webbrowsern). Diese Fragestellungen sind zu betrachten und durch geeignete Maßnahmen zu beantworten, wenn solche Systeme für die Arbeit mit sensiblen und vertraulichen Informationen eingesetzt werden sollen. Ziel der hier vorgestellten Arbeit ist es, Instant-Messaging-Systeme so zu gestalten, dass durch die Konzeption (bzw. Erweiterung) von geeigneten Sicherheitsmechanismen einerseits die einfache und spontane Nutzung der Systeme möglich bleibt und andererseits trotzdem eine sichere, authentifizierte und verbindliche Kollaboration unterstützt wird.
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.
This Thesis contributes by reporting on the current state of diffusion of collaboration information technology (CIT). The investigation concludes, with a high degree of certainty, that today we have a "satisfactory" diffusion level of some level-A CITs (mostly e-Mail, distantly followed by Audio Conferencing), and a "dissatisfactory" diffusion level of higher-level CITs (i.e. those requiring significant collaboration and cooperation among users, like Meeting Support Systems, Group Decision Support Systems, etc.). The potential benefits of the latter seem to be far from fully realised due to lack of user acceptance. This conclusion has gradually developed along the research cycle " it was suggested by Empirical Study I, and tested through Empirical Studies II and III. An additional, unplanned and rather interesting, finding from this study has been the recognition of large [mostly business] reporting on numerous Web 2.0 user-community produced collaboration technologies (most of them belonging to the category of "social software") and their metamorphosis from autonomous, "bottom-up" solutions into enterprise-supported infrastructures. Another contribution of this Thesis " again suggested by Empirical Study I, and tested through Empirical Studies II and III " pertains to the "process structure" of CIT diffusion. I have found that collaboration technology has historically diffused following two distinct (interdependent but orthogonal) diffusion paths " top-down (authority-based) and bottom-up. The authority-based diffusion path seems to be characterised by efforts aimed at "imposing" technologies on employees, the primary concern being to make sure that technology seamlessly and easily integrates into the organisational IT infrastructure. On the other hand, the bottom-up diffusion trail seems to be successful. The contribution of this investigation may be summarised as threefold: 1. This investigation consolidates most of the findings to date, pertaining to CIT adoption and diffusion, which have been produced by the CIT research community. Thus, it tells a coherent story of the dynamics of the community focus and the collective wisdom gathered over a period of (at least) one decade. 2. This work offers a meaningful framework within which to analyse existing knowledge " and indeed extends that knowledge base by identifying persistent problems of collaboration technology acceptance, adoption and diffusion. These problems have been repeatedly observed in practice, though the pattern does not seem to have been recognised and internalised by the community. Many of these problems have been observed in cases of CIT use one decade ago, five years ago, three years ago, and continue to be observed today in structurally the same form despite what is unarguably "rapid technological development". This gives me reason to believe that, at least some of the persistent problems of CIT diffusion can be hypothesised as "determining factors". My contribution here is to identify these factors, discuss them in detail, and thus tackle the theme of CIT diffusion through a structured historical narrative. 3. Through my contribution (2) above, I characterise a "knowledge-action gap" in the field of CIT and illuminate a potential path through which the research community might hope to bridge this gap. The gap may be operationalised as cognitive distance between CIT "knowledge" and CIT "action".
Im Rahmen dieser Arbeit wurden die zeitbewerteten Prädikat/Transitions-Netze (Z-Pr/T-Netze) zur Modellierung, Simulation und Verifikation sicherheitskritischer Echtzeitsysteme entwickelt. Z-Pr/T-Netze integrieren Konzepte zur Modellierung temporärer Zusammenhänge und sind darüber hinaus mittels der Berechnung von S- und T-Invarianten sowie der Identifikation von Traps und Co-Traps strukturell analysierbar. Die Eignung von Z-Pr/T-Netzen zur Modellierung, Simulation und Verifikation komplexer Systeme aus dem Anwendungsbereich sicherheitskritischer Echtzeitsysteme wird anhand des Earliest-Deadline-First-Protokolls (EDF) und des Priority-Inheritance-Protokolls (PIP) belegt. Es erfolgt daher eine Modellierung des EDF und PIP mittels Z-Pr/T-Netzen sowie eine Verifikation für das EDF und PIP basierend auf der strukturellen Analyse der korrespondierenden Z-Pr/T-Netze. Die Anwendbarkeit struktureller Analyseverfahren zur Verifikation des EDF und PIP in Verbindung mit der nicht zu unterschätzenden Komplexität eben dieser belegen die Anwendbarkeit von Z-Pr/T-Netzen zur Modellierung, Simulation und Verifikation komplexer Systeme aus dem Anwendungsbereich sicherheitskritischer Echtzeitsysteme.
Die Arbeit beschäftigt sich mit dem Einsatz moderner Grafikhardware (GPU) für die Visualisierung und Verarbeitung medizinischer Volumendaten. Die zunehmende Steigerung der Rechenleistung ermöglicht den Einsatz von Standardsystemen für Anwendungsgebiete, die bisher nur speziellen Workstations vorbehalten waren. Zusammen mit dem wesentlichen Vorteil von Grafikhardware Daten direkt anzeigen zu können, sind Verfahren wie visualisierungsgestütztes Berechnen ("visual computing") oder interaktives Steuern von Berechnungen ("computational steering") erst möglich geworden. Darauf wird anhand mehrerer Beispielanwendungen und umgesetzten Konzepten wie den "ray textures" im Detail eingegangen. Da die zu verarbeitenden und darzustellenden Datenmengen stetig ansteigen, ist aufgrund von Speicher- und Bandbreiteneinschränkungen eine kompakte Repräsentation der Daten notwendig. Während die Datenkompression selbst eingehend erforscht wurde, beschäftigt sich die vorliegende Arbeit mit Möglichkeiten, Berechnungen direkt auf den komprimierten Daten durchführen zu können. Dazu wurden verschiedene Algorithmenklassen identifiziert und in die Wavelet-Domäne übertragen. Mit Hilfe von speziellen Varianten der komprimierten Repräsentation ist eine effiziente Umsetzung grundlegender Bildverarbeitungsalgorithmen möglich und zeigt zugleich das Potential dieses Ansatzes auf. Aus technischer Sicht wurde im Laufe der Arbeit die GPU-basierte Programmierumgebung "Cascada" entwickelt. Sowohl die Einführung von objektorientierten Konzepten in die Shaderprogrammierung, als auch eine hierarchische Repräsentation von Berechnungs- und/oder Visualisierungsschritten vereinfacht den Einsatz von Grafikhardware ohne wesentliche Leistungseinbußen. Dies wird anhand verschiedener Implementationen in den jeweiligen Beiträgen und zwei klinischen Projekten im Bereich der Diagnoseunterstützung gezeigt. Hierbei geht es zum einen um die semi-automatische Segmentierung der Leber in niedrig aufgelösten MR-Datensätzen, zum anderen um Möglichkeiten zur Vermessung von abdominalen Aortenaneurysmen; jeweils unterstützt durch Grafikhardware. Darüber hinaus ermöglicht "cascada" auch die Erweiterung hinsichtlich aktueller Architekturen für den universellen Einsatz von Grafikhardware, sowie künftige Entwicklungen durch ein modulares Design.
In dieser Arbeit wurde untersucht, wie sich das bestehende Modell der Kabelsimulation verbessern lässt. Hierfür wurde zunächst analysiert, welches die Einflussfaktoren auf eine Simulation sind. Des Weiteren wurde der Einfluss der Rand- und Nebenbedingungen auf die Genauigkeit der Verlaufssimulation untersucht.
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.
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.
Probability propagation nets
(2008)
In der vorliegenden Arbeit wird eine Petri-Netz-Repräsentation für die Propagation von Wahrscheinlichkeiten und Evidenzen (Likelihoods) vorgestellt und auf probabilistische Horn-Abduktion sowie Fehlerbäume und Bayes-Netze angewendet. Diese sogenannten Wahrscheinlichkeits-Propagations-Netze (probability propagation nets) machen Propagations-Prozesse transparent, indem sie strukturelle und dynamische Aspekte in einer homogenen Darstellung vereinen. Anhand populärer Beispiele wird verdeutlicht, dass Wahrscheinlichkeits-Propagations-Netze die Propagations-Prozesse - besonders im Hinblick auf die Bayes-Netz-Algorithmik - anschaulich darstellen und gut nachvollziehbar machen, so dass sie sich für die Analyse und Diagnose probabilistischer Modelle eignen. Durch die Repräsentation von Fehlerbäumen mit Wahrscheinlichkeits-Propagations-Netzen können diese Vorzüge auf die Modellierung technischer Systeme übertragen werden.
In den letzten Jahren konzentrierte sich das E-Government auf die administrativen Aspekte der Verwaltungsmodernisierung. Im nächsten Schritt werden die E-Diskurse als Instrument der Bürgernähe und Mittel der E-Demokratie/E-Partizipation an Bedeutung gewinnen. Mit zunehmender Akzeptanz solcher E-Diskurse werden diese schnell eine Komplexität erreichen, die von den Teilnehmern nicht mehr zu bewältigen ist. Das Problem liegt in der eingeschränkten Möglichkeit, einen in Raum und Zeit verteilten Diskurs zu verfolgen und sich ein Bild von ihm zu machen. Viele Eindrücke, die sich aus Präsenzdiskussionen gewinnen lassen, fehlen. Deswegen hat die vorliegende Arbeit die Zielsetzung der Konzeption und der prototypischen Implementierung eines Instrumentariums (Diskursmeter), womit sich die Teilnehmer, insbesondere die Moderatoren, des E-Diskurses jederzeit einen Überblick über den E-Diskurs schaffen können und so zu ihrem Diskursverständnis (Discourse Awareness) zu gelangen. Über das aktuelle Geschehen im E-Diskurs informiert die gegenwartsorientierte und über das vergangene Geschehen die vergangenheitsorientierte Discourse Awareness, über die etwaige Trends sichtbar sind. Der Fokus der Discourse Awareness liegt in der quantitativen Betrachtung des Geschehens im E-Diskurs. Aus dem in dieser Arbeit entwickelten Modell des E-Diskurses resultieren die Fragestellungen zur Discourse Awareness, deren Konkretisierung Grundlage für die Implementierung des Diskursmeters ist. Die an das Modell des E-Diskurses angebrachten Diskurssensoren zeichnen das Geschehen im E-Diskurs auf, die zu Diskursereignissen führen, die das Diskursmeter in unterschiedlichen Visualisierungsformen präsentiert. Den Moderatoren des E-Diskurses bietet das Diskursmeter die gegenwartsorientierte Discourse Awareness als Monitoring und die vergangenheitsorientierte Discourse Awareness als Abfrage (quantitative Analyse) an.