TY - THES A1 - Wang, Long T1 - X-tracking the usage interest on web sites T1 - X-tracking des Nutzungsinteresses für Webseiten N2 - The exponential expanding of the numbers of web sites and Internet users makes WWW the most important global information resource. From information publishing and electronic commerce to entertainment and social networking, the Web allows an inexpensive and efficient access to the services provided by individuals and institutions. The basic units for distributing these services are the web sites scattered throughout the world. However, the extreme fragility of web services and content, the high competence between similar services supplied by different sites, and the wide geographic distributions of the web users drive the urgent requirement from the web managers to track and understand the usage interest of their web customers. This thesis, "X-tracking the Usage Interest on Web Sites", aims to fulfill this requirement. "X" stands two meanings: one is that the usage interest differs from various web sites, and the other is that usage interest is depicted from multi aspects: internal and external, structural and conceptual, objective and subjective. "Tracking" shows that our concentration is on locating and measuring the differences and changes among usage patterns. This thesis presents the methodologies on discovering usage interest on three kinds of web sites: the public information portal site, e-learning site that provides kinds of streaming lectures and social site that supplies the public discussions on IT issues. On different sites, we concentrate on different issues related with mining usage interest. The educational information portal sites were the first implementation scenarios on discovering usage patterns and optimizing the organization of web services. In such cases, the usage patterns are modeled as frequent page sets, navigation paths, navigation structures or graphs. However, a necessary requirement is to rebuild the individual behaviors from usage history. We give a systematic study on how to rebuild individual behaviors. Besides, this thesis shows a new strategy on building content clusters based on pair browsing retrieved from usage logs. The difference between such clusters and the original web structure displays the distance between the destinations from usage side and the expectations from design side. Moreover, we study the problem on tracking the changes of usage patterns in their life cycles. The changes are described from internal side integrating conceptual and structure features, and from external side for the physical features; and described from local side measuring the difference between two time spans, and global side showing the change tendency along the life cycle. A platform, Web-Cares, is developed to discover the usage interest, to measure the difference between usage interest and site expectation and to track the changes of usage patterns. E-learning site provides the teaching materials such as slides, recorded lecture videos and exercise sheets. We focus on discovering the learning interest on streaming lectures, such as real medias, mp4 and flash clips. Compared to the information portal site, the usage on streaming lectures encapsulates the variables such as viewing time and actions during learning processes. The learning interest is discovered in the form of answering 6 questions, which covers finding the relations between pieces of lectures and the preference among different forms of lectures. We prefer on detecting the changes of learning interest on the same course from different semesters. The differences on the content and structure between two courses leverage the changes on the learning interest. We give an algorithm on measuring the difference on learning interest integrated with similarity comparison between courses. A search engine, TASK-Moniminer, is created to help the teacher query the learning interest on their streaming lectures on tele-TASK site. Social site acts as an online community attracting web users to discuss the common topics and share their interesting information. Compared to the public information portal site and e-learning web site, the rich interactions among users and web content bring the wider range of content quality, on the other hand, provide more possibilities to express and model usage interest. We propose a framework on finding and recommending high reputation articles in a social site. We observed that the reputation is classified into global and local categories; the quality of the articles having high reputation is related with the content features. Based on these observations, our framework is implemented firstly by finding the articles having global or local reputation, and secondly clustering articles based on their content relations, and then the articles are selected and recommended from each cluster based on their reputation ranks. N2 - Wegen des exponentiellen Ansteigens der Anzahl an Internet-Nutzern und Websites ist das WWW (World Wide Web) die wichtigste globale Informationsressource geworden. Das Web bietet verschiedene Dienste (z. B. Informationsveröffentlichung, Electronic Commerce, Entertainment oder Social Networking) zum kostengünstigen und effizienten erlaubten Zugriff an, die von Einzelpersonen und Institutionen zur Verfügung gestellt werden. Um solche Dienste anzubieten, werden weltweite, vereinzelte Websites als Basiseinheiten definiert. Aber die extreme Fragilität der Web-Services und -inhalte, die hohe Kompetenz zwischen ähnlichen Diensten für verschiedene Sites bzw. die breite geographische Verteilung der Web-Nutzer treiben einen dringenden Bedarf für Web-Manager und das Verfolgen und Verstehen der Nutzungsinteresse ihrer Web-Kunden. Die Arbeit zielt darauf ab, dass die Anforderung "X-tracking the Usage Interest on Web Sites" erfüllt wird. "X" hat zwei Bedeutungen. Die erste Bedeutung ist, dass das Nutzungsinteresse von verschiedenen Websites sich unterscheidet. Außerdem stellt die zweite Bedeutung dar, dass das Nutzungsinteresse durch verschiedene Aspekte (interne und externe, strukturelle und konzeptionelle) beschrieben wird. Tracking zeigt, dass die Änderungen zwischen Nutzungsmustern festgelegt und gemessen werden. Die Arbeit eine Methodologie dar, um das Nutzungsinteresse gekoppelt an drei Arten von Websites (Public Informationsportal-Website, E-Learning-Website und Social-Website) zu finden. Wir konzentrieren uns auf unterschiedliche Themen im Bezug auf verschieden Sites, die mit Usage-Interest-Mining eng verbunden werden. Education Informationsportal-Website ist das erste Implementierungsscenario für Web-Usage-Mining. Durch das Scenario können Nutzungsmuster gefunden und die Organisation von Web-Services optimiert werden. In solchen Fällen wird das Nutzungsmuster als häufige Pagemenge, Navigation-Wege, -Strukturen oder -Graphen modelliert. Eine notwendige Voraussetzung ist jedoch, dass man individuelle Verhaltensmuster aus dem Verlauf der Nutzung (Usage History) wieder aufbauen muss. Deshalb geben wir in dieser Arbeit eine systematische Studie zum Nachempfinden der individuellen Verhaltensweisen. Außerdem zeigt die Arbeit eine neue Strategie, dass auf Page-Paaren basierten Content-Clustering aus Nutzungssite aufgebaut werden. Der Unterschied zwischen solchen Clustern und der originalen Webstruktur ist der Abstand zwischen Zielen der Nutzungssite und Erwartungen der Designsite. Darüber hinaus erforschen wir Probleme beim Tracking der Änderungen von Nutzungsmustern in ihrem Lebenszyklus. Die Änderungen werden durch mehrere Aspekte beschrieben. Für internen Aspekt werden konzeptionelle Strukturen und Funktionen integriert. Der externe Aspekt beschreibt physische Eigenschaften. Für lokalen Aspekt wird die Differenz zwischen zwei Zeitspannen gemessen. Der globale Aspekt zeigt Tendenzen der Änderung entlang des Lebenszyklus. Eine Plattform "Web-Cares" wird entwickelt, die die Nutzungsinteressen findet, Unterschiede zwischen Nutzungsinteresse und Website messen bzw. die Änderungen von Nutzungsmustern verfolgen kann. E-Learning-Websites bieten Lernmaterialien wie z.B. Folien, erfaßte Video-Vorlesungen und Übungsblätter an. Wir konzentrieren uns auf die Erfoschung des Lerninteresses auf Streaming-Vorlesungen z.B. Real-Media, mp4 und Flash-Clips. Im Vergleich zum Informationsportal Website kapselt die Nutzung auf Streaming-Vorlesungen die Variablen wie Schauzeit und Schautätigkeiten während der Lernprozesse. Das Lerninteresse wird erfasst, wenn wir Antworten zu sechs Fragen gehandelt haben. Diese Fragen umfassen verschiedene Themen, wie Erforschung der Relation zwischen Teilen von Lehrveranstaltungen oder die Präferenz zwischen den verschiedenen Formen der Lehrveranstaltungen. Wir bevorzugen die Aufdeckung der Veränderungen des Lerninteresses anhand der gleichen Kurse aus verschiedenen Semestern. Der Differenz auf den Inhalt und die Struktur zwischen zwei Kurse beeinflusst die Änderungen auf das Lerninteresse. Ein Algorithmus misst die Differenz des Lerninteresses im Bezug auf einen Ähnlichkeitsvergleich zwischen den Kursen. Die Suchmaschine „Task-Moniminer“ wird entwickelt, dass die Lehrkräfte das Lerninteresse für ihre Streaming-Vorlesungen über das Videoportal tele-TASK abrufen können. Social Websites dienen als eine Online-Community, in den teilnehmenden Web-Benutzern die gemeinsamen Themen diskutieren und ihre interessanten Informationen miteinander teilen. Im Vergleich zur Public Informationsportal-Website und E-Learning Website bietet diese Art von Website reichhaltige Interaktionen zwischen Benutzern und Inhalten an, die die breitere Auswahl der inhaltlichen Qualität bringen. Allerdings bietet eine Social-Website mehr Möglichkeiten zur Modellierung des Nutzungsinteresses an. Wir schlagen ein Rahmensystem vor, die hohe Reputation für Artikel in eine Social-Website empfiehlt. Unsere Beobachtungen sind, dass die Reputation in globalen und lokalen Kategorien klassifiziert wird. Außerdem wird die Qualität von Artikeln mit hoher Reputation mit den Content-Funktionen in Zusammenhang stehen. Durch die folgenden Schritte wird das Rahmensystem im Bezug auf die Überwachungen implementiert. Der erste Schritt ist, dass man die Artikel mit globalen oder lokalen Reputation findet. Danach werden Artikel im Bezug auf ihre Content-Relationen in jeder Kategorie gesammelt. Zum Schluß werden die ausgewählten Artikel aus jedem basierend auf ihren Reputation-Ranking Cluster empfohlen. KW - Tracking KW - Nutzungsinteresse KW - Webseite KW - Tracking KW - Usage Interest KW - Web Sites Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-51077 ER - TY - THES A1 - Schrape, Oliver T1 - Methodology for standard cell-based design and implementation of reliable and robust hardware systems T1 - Methoden für Standardzellbasiertes Design und Implementierung zuverlässiger und robuster Hardware Systeme N2 - Reliable and robust data processing is one of the hardest requirements for systems in fields such as medicine, security, automotive, aviation, and space, to prevent critical system failures caused by changes in operating or environmental conditions. In particular, Signal Integrity (SI) effects such as crosstalk may distort the signal information in sensitive mixed-signal designs. A challenge for hardware systems used in the space are radiation effects. Namely, Single Event Effects (SEEs) induced by high-energy particle hits may lead to faulty computation, corrupted configuration settings, undesired system behavior, or even total malfunction. Since these applications require an extra effort in design and implementation, it is beneficial to master the standard cell design process and corresponding design flow methodologies optimized for such challenges. Especially for reliable, low-noise differential signaling logic such as Current Mode Logic (CML), a digital design flow is an orthogonal approach compared to traditional manual design. As a consequence, mandatory preliminary considerations need to be addressed in more detail. First of all, standard cell library concepts with suitable cell extensions for reliable systems and robust space applications have to be elaborated. Resulting design concepts at the cell level should enable the logical synthesis for differential logic design or improve the radiation-hardness. In parallel, the main objectives of the proposed cell architectures are to reduce the occupied area, power, and delay overhead. Second, a special setup for standard cell characterization is additionally required for a proper and accurate logic gate modeling. Last but not least, design methodologies for mandatory design flow stages such as logic synthesis and place and route need to be developed for the respective hardware systems to keep the reliability or the radiation-hardness at an acceptable level. This Thesis proposes and investigates standard cell-based design methodologies and techniques for reliable and robust hardware systems implemented in a conventional semi-conductor technology. The focus of this work is on reliable differential logic design and robust radiation-hardening-by-design circuits. The synergistic connections of the digital design flow stages are systematically addressed for these two types of hardware systems. In more detail, a library for differential logic is extended with single-ended pseudo-gates for intermediate design steps to support the logic synthesis and layout generation with commercial Computer-Aided Design (CAD) tools. Special cell layouts are proposed to relax signal routing. A library set for space applications is similarly extended by novel Radiation-Hardening-by-Design (RHBD) Triple Modular Redundancy (TMR) cells, enabling a one fault correction. Therein, additional optimized architectures for glitch filter cells, robust scannable and self-correcting flip-flops, and clock-gates are proposed. The circuit concepts and the physical layout representation views of the differential logic gates and the RHBD cells are discussed. However, the quality of results of designs depends implicitly on the accuracy of the standard cell characterization which is examined for both types therefore. The entire design flow is elaborated from the hardware design description to the layout representations. A 2-Phase routing approach together with an intermediate design conversion step is proposed after the initial place and route stage for reliable, pure differential designs, whereas a special constraining for RHBD applications in a standard technology is presented. The digital design flow for differential logic design is successfully demonstrated on a reliable differential bipolar CML application. A balanced routing result of its differential signal pairs is obtained by the proposed 2-Phase-routing approach. Moreover, the elaborated standard cell concepts and design methodology for RHBD circuits are applied to the digital part of a 7.5-15.5 MSPS 14-bit Analog-to-Digital Converter (ADC) and a complex microcontroller architecture. The ADC is implemented in an unhardened standard semiconductor technology and successfully verified by electrical measurements. The overhead of the proposed hardening approach is additionally evaluated by design exploration of the microcontroller application. Furthermore, the first obtained related measurement results of novel RHBD-∆TMR flip-flops show a radiation-tolerance up to a threshold Linear Energy Transfer (LET) of 46.1, 52.0, and 62.5 MeV cm2 mg-1 and savings in silicon area of 25-50 % for selected TMR standard cell candidates. As a conclusion, the presented design concepts at the cell and library levels, as well as the design flow modifications are adaptable and transferable to other technology nodes. In particular, the design of hybrid solutions with integrated reliable differential logic modules together with robust radiation-tolerant circuit parts is enabled by the standard cell concepts and design methods proposed in this work. N2 - Eine zuverlässige und robuste Datenverarbeitung ist eine der wichtigsten Voraussetzungen für Systeme in Bereichen wie Medizin, Sicherheit, Automobilbau, Luft- und Raumfahrt, um kritische Systemausfälle zu verhindern, welche durch Änderungen der Betriebsbedingung oder Umweltgegebenheiten hervorgerufen werden können. Insbesondere Signalintegritätseffekte (Signal Integrity (SI)) wie das Übersprechen und Überlagern von Signalen (crosstalk) können den Informationsgehalt in empfindlichen Mixed-Signal-Designs verzerren. Eine zusätzliche Herausforderung für Hardwaresysteme für Weltraumanwendungen ist die Strahlung. Resultierende Effekte, die durch hochenergetische Teilchentreffer ausgelöst werden (Single Event Effects (SEEs)), können zu fehlerhaften Berechnungen, beschädigten Konfigurationseinstellungen, unerwünschtem Systemverhalten oder sogar zu völliger Fehlfunktion führen. Da diese Anwendungen einen zusätzlichen Aufwand beim Entwurf und der Implementierung erfordern, ist es von Vorteil, über Standardzellenentwurfskonzepte und entsprechende Entwurfsablaufmethoden zu verfügen, die für genau solche Herausforderungen optimiert sind. Insbesondere für zuverlässige, rauscharme differenzielle Logik, wie der Current Mode Logic (CML), ist ein digitaler Entwurfsablauf ein orthogonaler Ansatz im Vergleich zum traditionellen manuellen Entwurfskonzept. Infolgedessen müssen obligatorische Vorüberlegungen detaillierter behandelt werden. Zunächst sind Konzepte für Standardzellbibliotheken mit geeigneten Zellerweiterungen für zuverlässige Systeme und robuste Raumfahrtanwendungen zu erarbeiten. Daraus resultierende Entwurfskonzepte auf Zellebene sollten die logische Synthese für den differenziellen Logikentwurf ermöglichen oder die Strahlungshärte eines Designs verbessern. Parallel dazu sind die Hauptziele der vorgeschlagenen Zellarchitekturen, die Verringerung der genutzten Siliziumfläche und der Verlustleistung sowie den Verzögerungs-Overhead zu minimieren. Zweitens ist ein spezieller Aufbau für die Charakterisierung von Standardzellen erforderlich, um eine angemessene und genaue Modellierung der Logikgatter zu ermöglichen. Nicht zuletzt müssen für die jeweiligen Hardwaresysteme Methoden für die Entwurfsphasen wie Logik-Synthese und das Platzieren und Routen (Place and Route (PnR)) entwickelt werden, um die Zuverlässigkeit beziehungsweise die Strahlungshärte auf einem akzeptablen Niveau zu halten. In dieser Arbeit werden standardisierte Zellen-basierte Entwurfsmethoden und -techniken für zuverlässige und robuste Hardwaresysteme vorgeschlagen und untersucht, welche in einer herkömmlichen Halbleitertechnologie implementiert werden. Dabei werden zuverlässige differenzielle Logikschaltungen und robuste strahlungsgehärtete Schaltungen betrachtet. Die synergetischen Verbindungen des digitalen Entwurfs werden systematisch für diese beiden Hardwaresysteme behandelt. Im Detail wird eine Bibliothek für differentielle Logik mit Single-Ended-Pseudo-Gattern für Zwischenschritte erweitert, die die Logiksynthese und Layout-Generierung mit heutigen Entwicklungswerkzeugen unterstützen. Ein spezieller Rahmen für das Layout der Zellen wird vorgeschlagen, um das Routing der Signale zu vereinfachen. Die Bibliothek für Raumfahrtanwendungen wird in ähnlicher Weise um neuartige Radiation-Hardening-by-Design (RHBD)-Zellen mit dreifacher modularer Redundanz (Triple Modular Redundancy (TMR)) erweitert, welche eine 1-Bit-Fehlerkorrektur erlaubt. Zusätzlich werden optimierte Architekturen für Glitch-Filterzellen, robuste abtastbare (scannable) und selbstkorrigierende Flip-flops und Taktgatter (clock-gates) vorgeschlagen. Die Schaltungskonzepte, die physische Layout-Repräsentation der differentiellen Logikgatter und der vorgeschlagenen RHBD-Zellen werden diskutiert. Die Qualität der Ergebnisse der Entwürfe hängt jedoch implizit von der Genauigkeit der Standardzellencharakterisierung ab, die daher für beide Typen untersucht wird. Der gesamte Entwurfsablauf wird von der Entwurfsbeschreibung der Hardware bis hin zur generierten Layout-Darstellung ausgearbeitet. Infolgedessen wird ein 2-Phasen-Routing-Ansatz zusammen mit einem zwischengeschalteten Design-Konvertierungsschritt nach der initialen PnR-Phase für zuverlässige, differentielle Designs vorgeschlagen, während ein spezielles Constraining für RHBD-Anwendungen vorgestellt wird. Der digitale Entwurfsablauf für Differenziallogik wird erfolgreich an einer zuverlässigen bipolaren Differenzial-CML-Anwendung demonstriert. Durch den 2-Phasen-Routing-Ansatz wird ein ausgewogenes Routing-Ergebnis differentieller Signalpaare erzielt. Darüber hinaus werden die erarbeiteten Standardzellenkonzepte und die Entwurfsmethodik für RHBD-Schaltungen auf den digitalen Teil eines 7.5-15.5MSPS 14-bit Analog-Digital-Wandlers (ADC) und einer komplexen Mikrocontroller-Architektur angewandt. Der ADC wurde in einer nicht-gehärteten Standard-Halbleitertechnologie implementiert und erfolgreich durch elektrische Messungen verifiziert. Der Mehraufwand des Härtungsansatzes wird zusätzlich durch Design Exploration der Mikrocontroller-Anwendung bewertet. Ferner zeigen erste Messergebnisse der neuartigen RHBD-ΔTMR-Flip-flops eine Strahlungstoleranz bis zu einem linearen Energietransfer (Linear Energy Transfers (LET)) Schwellwert von 46.1, 52.0 und 62.5MeVcm2 mg-1 und eine Einsparung an Siliziumfläche von 25-50% für ausgewählte TMR-Standardzellenkandidaten. Die vorgestellten Entwurfskonzepte auf Zell- und Bibliotheksebene sowie die Änderungen des Entwurfsablaufs sind anpassbar und übertragbar auf andere Technologieknoten. Insbesondere der Entwurf hybrider Lösungen mit integrierten zuverlässigen differenziellen Logikmodulen zusammen mit robusten strahlungstoleranten Schaltungsteilen wird durch die in dieser Arbeit vorgeschlagenen Konzepte und Entwurfsmethoden ermöglicht. KW - hardware design KW - ASIC KW - radiation hardness KW - digital design KW - ASIC (Applikationsspezifische Integrierte Schaltkreise) KW - Digital Design KW - Hardware Design KW - Strahlungshartes Design Y1 - 2023 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-589326 ER - TY - THES A1 - Seuring, Markus T1 - Output space compaction for testing and concurrent checking N2 - In der Dissertation werden neue Entwurfsmethoden für Kompaktoren für die Ausgänge von digitalen Schaltungen beschrieben, die die Anzahl der zu testenden Ausgänge drastisch verkleinern und dabei die Testbarkeit der Schaltungen nur wenig oder gar nicht verschlechtern. Der erste Teil der Arbeit behandelt für kombinatorische Schaltungen Methoden, die die Struktur der Schaltungen beim Entwurf der Kompaktoren berücksichtigen. Verschiedene Algorithmen zur Analyse von Schaltungsstrukturen werden zum ersten Mal vorgestellt und untersucht. Die Komplexität der vorgestellten Verfahren zur Erzeugung von Kompaktoren ist linear bezüglich der Anzahl der Gatter in der Schaltung und ist damit auf sehr große Schaltungen anwendbar. Im zweiten Teil wird erstmals ein solches Verfahren für sequentielle Schaltkreise beschrieben. Dieses Verfahren baut im wesentlichen auf das erste auf. Der dritte Teil beschreibt eine Entwurfsmethode, die keine Informationen über die interne Struktur der Schaltung oder über das zugrundeliegende Fehlermodell benötigt. Der Entwurf basiert alleine auf einem vorgegebenen Satz von Testvektoren und die dazugehörenden Testantworten der fehlerfreien Schaltung. Ein nach diesem Verfahren erzeugter Kompaktor maskiert keinen der Fehler, die durch das Testen mit den vorgegebenen Vektoren an den Ausgängen der Schaltung beobachtbar sind. N2 - The objective of this thesis is to provide new space compaction techniques for testing or concurrent checking of digital circuits. In particular, the work focuses on the design of space compactors that achieve high compaction ratio and minimal loss of testability of the circuits. In the first part, the compactors are designed for combinational circuits based on the knowledge of the circuit structure. Several algorithms for analyzing circuit structures are introduced and discussed for the first time. The complexity of each design procedure is linear with respect to the number of gates of the circuit. Thus, the procedures are applicable to large circuits. In the second part, the first structural approach for output compaction for sequential circuits is introduced. Essentially, it enhances the first part. For the approach introduced in the third part it is assumed that the structure of the circuit and the underlying fault model are unknown. The space compaction approach requires only the knowledge of the fault-free test responses for a precomputed test set. The proposed compactor design guarantees zero-aliasing with respect to the precomputed test set. KW - digital circuit KW - output space compaction KW - zero-aliasing KW - test KW - concurrent checking KW - propagation probability KW - IP core Y1 - 2000 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-0000165 ER - TY - THES A1 - Chen, Junchao T1 - A self-adaptive resilient method for implementing and managing the high-reliability processing system T1 - Eine selbstadaptive belastbare Methode zum Implementieren und Verwalten von hochzuverlässigen Verarbeitungssysteme N2 - As a result of CMOS scaling, radiation-induced Single-Event Effects (SEEs) in electronic circuits became a critical reliability issue for modern Integrated Circuits (ICs) operating under harsh radiation conditions. SEEs can be triggered in combinational or sequential logic by the impact of high-energy particles, leading to destructive or non-destructive faults, resulting in data corruption or even system failure. Typically, the SEE mitigation methods are deployed statically in processing architectures based on the worst-case radiation conditions, which is most of the time unnecessary and results in a resource overhead. Moreover, the space radiation conditions are dynamically changing, especially during Solar Particle Events (SPEs). The intensity of space radiation can differ over five orders of magnitude within a few hours or days, resulting in several orders of magnitude fault probability variation in ICs during SPEs. This thesis introduces a comprehensive approach for designing a self-adaptive fault resilient multiprocessing system to overcome the static mitigation overhead issue. This work mainly addresses the following topics: (1) Design of on-chip radiation particle monitor for real-time radiation environment detection, (2) Investigation of space environment predictor, as support for solar particle events forecast, (3) Dynamic mode configuration in the resilient multiprocessing system. Therefore, according to detected and predicted in-flight space radiation conditions, the target system can be configured to use no mitigation or low-overhead mitigation during non-critical periods of time. The redundant resources can be used to improve system performance or save power. On the other hand, during increased radiation activity periods, such as SPEs, the mitigation methods can be dynamically configured appropriately depending on the real-time space radiation environment, resulting in higher system reliability. Thus, a dynamic trade-off in the target system between reliability, performance and power consumption in real-time can be achieved. All results of this work are evaluated in a highly reliable quad-core multiprocessing system that allows the self-adaptive setting of optimal radiation mitigation mechanisms during run-time. Proposed methods can serve as a basis for establishing a comprehensive self-adaptive resilient system design process. Successful implementation of the proposed design in the quad-core multiprocessor shows its application perspective also in the other designs. N2 - Infolge der CMOS-Skalierung wurden strahleninduzierte Einzelereignis-Effekte (SEEs) in elektronischen Schaltungen zu einem kritischen Zuverlässigkeitsproblem für moderne integrierte Schaltungen (ICs), die unter rauen Strahlungsbedingungen arbeiten. SEEs können in der kombinatorischen oder sequentiellen Logik durch den Aufprall hochenergetischer Teilchen ausgelöst werden, was zu destruktiven oder nicht-destruktiven Fehlern und damit zu Datenverfälschungen oder sogar Systemausfällen führt. Normalerweise werden die Methoden zur Abschwächung von SEEs statisch in Verarbeitungsarchitekturen auf der Grundlage der ungünstigsten Strahlungsbedingungen eingesetzt, was in den meisten Fällen unnötig ist und zu einem Ressourcen-Overhead führt. Darüber hinaus ändern sich die Strahlungsbedingungen im Weltraum dynamisch, insbesondere während Solar Particle Events (SPEs). Die Intensität der Weltraumstrahlung kann sich innerhalb weniger Stunden oder Tage um mehr als fünf Größenordnungen ändern, was zu einer Variation der Fehlerwahrscheinlichkeit in ICs während SPEs um mehrere Größenordnungen führt. In dieser Arbeit wird ein umfassender Ansatz für den Entwurf eines selbstanpassenden, fehlerresistenten Multiprozessorsystems vorgestellt, um das Problem des statischen Mitigation-Overheads zu überwinden. Diese Arbeit befasst sich hauptsächlich mit den folgenden Themen: (1) Entwurf eines On-Chip-Strahlungsteilchen Monitors zur Echtzeit-Erkennung von Strahlung Umgebungen, (2) Untersuchung von Weltraumumgebungsprognosen zur Unterstützung der Vorhersage von solaren Teilchen Ereignissen, (3) Konfiguration des dynamischen Modus in einem belastbaren Multiprozessorsystem. Daher kann das Zielsystem je nach den erkannten und vorhergesagten Strahlungsbedingungen während des Fluges so konfiguriert werden, dass es während unkritischer Zeiträume keine oder nur eine geringe Strahlungsminderung vornimmt. Die redundanten Ressourcen können genutzt werden, um die Systemleistung zu verbessern oder Energie zu sparen. In Zeiten erhöhter Strahlungsaktivität, wie z. B. während SPEs, können die Abschwächungsmethoden dynamisch und in Abhängigkeit von der Echtzeit-Strahlungsumgebung im Weltraum konfiguriert werden, was zu einer höheren Systemzuverlässigkeit führt. Auf diese Weise kann im Zielsystem ein dynamischer Kompromiss zwischen Zuverlässigkeit, Leistung und Stromverbrauch in Echtzeit erreicht werden. Alle Ergebnisse dieser Arbeit wurden in einem hochzuverlässigen Quad-Core-Multiprozessorsystem evaluiert, das die selbstanpassende Einstellung optimaler Strahlungsschutzmechanismen während der Laufzeit ermöglicht. Die vorgeschlagenen Methoden können als Grundlage für die Entwicklung eines umfassenden, selbstanpassenden und belastbaren Systementwurfsprozesses dienen. Die erfolgreiche Implementierung des vorgeschlagenen Entwurfs in einem Quad-Core-Multiprozessor zeigt, dass er auch für andere Entwürfe geeignet ist. KW - single event upset KW - solar particle event KW - machine learning KW - self-adaptive multiprocessing system KW - maschinelles Lernen KW - selbstanpassendes Multiprozessorsystem KW - strahleninduzierte Einzelereignis-Effekte KW - Sonnenteilchen-Ereignis Y1 - 2023 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-583139 ER - TY - THES A1 - Frank, Mario T1 - On synthesising Linux kernel module components from Coq formalisations T1 - Über die Synthese von Linux Kernel- Modul-Komponenten aus Coq-Formalisierungen N2 - This thesis presents an attempt to use source code synthesised from Coq formalisations of device drivers for existing (micro)kernel operating systems, with a particular focus on the Linux Kernel. In the first part, the technical background and related work are described. The focus is here on the possible approaches to synthesising certified software with Coq, namely the extraction to functional languages using the Coq extraction plugin and the extraction to Clight code using the CertiCoq plugin. It is noted that the implementation of CertiCoq is verified, whereas this is not the case for the Coq extraction plugin. Consequently, there is a correctness guarantee for the generated Clight code which does not hold for the code being generated by the Coq extraction plugin. Furthermore, the differences between user space and kernel space software are discussed in relation to Linux device drivers. It is elaborated that it is not possible to generate working Linux kernel module components using the Coq extraction plugin without significant modifications. In contrast, it is possible to produce working user space drivers both with the Coq extraction plugin and CertiCoq. The subsequent parts describe the main contributions of the thesis. In the second part, it is demonstrated how to extend the Coq extraction plugin to synthesise foreign function calls between the functional language OCaml and the imperative language C. This approach has the potential to improve the type-safety of user space drivers. Furthermore, it is shown that the code being synthesised by CertiCoq cannot be used in kernel space without modifications to the necessary runtime. Consequently, the necessary modifications to the runtimes of CertiCoq and VeriFFI are introduced, resulting in the runtimes becoming compatible components of a Linux kernel module. Furthermore, justifications for the transformations are provided and possible further extensions to both plugins and solutions to failing garbage collection calls in kernel space are discussed. The third part presents a proof of concept device driver for the Linux Kernel. To achieve this, the event handler of the original PC Speaker driver is partially formalised in Coq. Furthermore, some relevant formal properties of the formalised functionality are discussed. Subsequently, a kernel module is defined, utilising the modified variants of CertiCoq and VeriFFI to compile a working device driver. It is furthermore shown that it is possible to compile the synthesised code with CompCert, thereby extending the guarantee of correctness to the assembly layer. This is followed by a performance evaluation that compares a naive formalisation of the PC speaker functionality with the original PC Speaker driver pointing out the weaknesses in the formalisation and possible improvements. The part closes with a summary of the results, their implications and open questions being raised. The last part lists all used sources, separated into scientific literature, documentations or reference manuals and artifacts, i.e. source code. N2 - Die vorliegende Dissertation präsentiert einen Ansatz zur Nutzung von Quellcode, der aus der Coq-Formalisierung eines Gerätetreibers generiert wurde, für bestehende (Mikrokernel-)Betriebssysteme, im Speziellen den Linux-Kernel. Im ersten Teil erfolgt eine Beschreibung der relevanten technischen Aspekte sowie des aktuellen Forschungsstandes. Dabei liegt der Fokus auf der Synthese von funktionalem Code durch das Coq Extraction Plugin und von Clight Code durch das CertiCoq Plugin. Des Weiteren wird dargelegt, dass die Implementierung von CertiCoq im Gegensatz zu der des Coq Extraction Plugin verifiziert ist, wodurch sich eine Korrektheitsgarantie für den generierten Clight Code ableiten lässt. Darüber hinaus werden die Unterschiede zwischen User Space und Kernel Space Software in Bezug auf Linux-Treiber erörtert. Unter Berücksichtigung der technischen Einschränkungen wird dargelegt, dass der durch das Coq Extraction Plugin generierte Code ohne gravierende Anpassungen der Laufzeitumgebung nicht als Teil eines Kernel Space Treibers nutzbar ist. Die nachfolgenden Teile der Dissertation behandeln den Beitrag dieser Arbeit. Im zweiten Teil wird dargelegt, wie das Coq Extraction Plugin derart erweitert werden kann, dass typsichere Aufrufe zwischen den Sprachen OCaml und C generiert werden können. Dies verhindert spezifische Kompilationsfehler aufgrund von Typfehlern. Des Weiteren wird aufgezeigt, dass der durch CertiCoq generierte Code ebenfalls nicht im Kernel Space genutzt werden kann, da die Laufzeitumgebung technische Einschränkungen verletzt. Daher werden die notwendigen Anpassungen an der vergleichsweise kleinen Laufzeitumgebung sowie an VeriFFI vorgestellt und deren Korrektheit begründet. Anschließend werden mögliche Erweiterungen beider Plugins sowie die Möglichkeit der Behandlung von fehlschlagenden Aufrufen der Garbage Collection von CertiCoq im Kernel Space erörtert. Im dritten Teil wird als Machbarkeitsstudie im ersten Schritt der Event-Handler des Linux PC Speaker Treibers beschrieben und eine naive Coq-Formalisierung sowie wichtige formale Eigenschaften dargelegt. Dann wird beschrieben, wie ein Kernel-Modul und dessen Kompilation definiert werden muss, um einen lauffähigen Linux Kernel Treiber zu erhalten. Des Weiteren wird erläutert, wie die generierten Teile dieses Treibers mit dem verifizierten Kompiler CompCert übersetzt werden können, wodurch auch eine Korrektheit für den resultierenden Assembler-Code gilt. Im Anschluss erfolgt eine Evaluierung der Performance des aus der naiven Coq-Formalisierung generierten Codes im Vergleich zum originalen PC-Speaker Treiber. Dabei werden die Schwächen der Formalisierung sowie mögliche Verbesserungen diskutiert. Der Teil wird mit einer Zusammenfassung der Ergebnisse sowie der daraus resultierenden offenen Fragen abgeschlossen. Der letzte Teil gibt eine Übersicht über genutzte Quellen und Hilfsmittel, unterteilt in wissenschaftliche Literatur, Dokumentationen sowie Software-Artefakte. KW - Linux device drivers KW - Coq KW - CertiCoq KW - synthesis KW - compilation KW - Geräte-Treiber KW - Linux KW - Coq KW - CertiCoq KW - Synthese KW - Kompilation Y1 - 2024 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-642558 ER -