TY - THES A1 - Müller, Sebastian T1 - Software-basierte Rekonfiguration in statisch geplanten Mehrkernsystemen zur Behandlung permanenter Fehler T1 - Software-Based Self-Repair of Statically Scheduled Multi-Core Systems for Handling Permanent Faults N2 - In zukünftigen eingebetteten Systemen ist bei zunehmender Integrationsdichte mit einer abnehmenden Zuverlässigkeit zu rechnen. Insbesondere lang laufende Systeme werden mit fortschreitender Zeit Alterungserscheinungen aufweisen, die sich durch den permanenten Ausfall einzelner Komponenten bemerkbar machen. Um die Funktionstüchtigkeit solcher Systeme auch für einen langen Zeitraum zu gewährleisten, sind Funktionen erforderlich, die die Erkennung, Lokalisierung und Behandlung solcher permanenter Fehler erlauben. Diese Funktionen sind dabei in das System zu integrieren. Es existieren dafür bereits verschiedene Ansätze auf unterschiedlichen Systemebenen. Das Spektrum solcher Ansätze reicht von einer Reparatur auf Transistorebene über die Reparatur einzelner Komponenten, die aus einigen dutzend bis einigen tausend Transistoren bestehen, bis hin zu Reparaturansätzen, die komplette Prozessorkerne in einem System ersetzen. Jeder Ansatz hat dabei seine spezifischen Vor- und Nachteile. Das betrifft insbesondere den Aufwand zur Administration der Reparatur sowie die Anwendbarkeit auf beliebige Hardwarestrukturen. Bisher wurden die Reparaturmethoden isoliert entwickelt. In Systemen mit zunehmender Komplexität wird jedoch ein hierarchischer Ansatz benötigt, der die existierenden Techniken ebenenübergreifend verbindet. Dadurch kann eine Zerlegung des Systems in verschiedene Gruppen vorgenommen werden, wobei für jede Gruppe eine spezifische Reparaturmethodik besonders geeignet ist. Es entsteht dadurch ein teils hierarchisch organisierter Reparaturansatz, der unterschiedliche Reparaturtechniken miteinander kombiniert. Es werden für das hierarchische Verfahren insbesondere software-basierte Reparaturansätze betrachtet, da diese nur einen geringen Administrationsaufwand in Hardware erfordern. Die Nutzung fehlerhafter Komponenten im Prozessor wird dabei durch die Anpassung des ausgeführten Programms an die aktuelle Fehlersituation vermieden. Diese Anpassung kann beispielsweise auf Systemebene, durch Verlagerung eines Programms von einem Prozessorkern auf einen anderen Kern oder auf der Ebene von Prozessorkernen, wobei die Benutzung einzelner Komponenten eines Kerns vermieden wird, erfolgen. Diese Anpassungen lassen sich durch Techniken, wie sie im Backend eines Compilers eingesetzt werden, bewerkstelligen. Die Reparatur auf den verschiedenen Ebenen erfordert dabei unterschiedlich mächtige Backends. Das reicht von einem Backend, das nur eine Ablaufplanung ändert, über ein Backend, das darüber hinaus noch die Registervergabe anpasst, bis hin zu einem Backend, das den Programmcode zweier Prozessorkerne vertauscht und an den jeweiligen Kern anpasst. Die Ausführung der software-basierten Reparatur soll dabei möglichst durch den fehlerhaften Kern selbst ausgeführt werden. In schwerwiegenden Fällen erfolgt eine administrierte Reparatur auf der Systemebene durch einen zur Reparaturzeit bestimmten Prozessorkern des Systems. Der Aufwand für entsprechende Backends sowie deren Möglichkeit zur Fehlerbehandlung werden in dieser Arbeit untersucht. N2 - Due to the shrinking feature-size of integrated circuits a lower reliability is predicted for embedded systems. The higher stress density in those circuits leads to wear-out effects, which result in a permanent fault of processor components. In order to ensure a certain quality of service for long-term systems, techniques for fault detection, localization and error handling have to be integrated into a system. Several approaches are already known for different hierarchical levels of a system. Those approaches can replace hardware structure with a size from hundred to thousands of transistors or can even exchange entire processor cores with spare-cores. Every approach has its own advantage and draw-back. The key issues are the overhead for administrating a repair and the applicability for any hardware structure of a processor. Due to the increasing complexity of modern embedded systems a hierarchical approach is required, which combines the existing techniques in one approach. This offers the possibility to separate a system into different levels. A dedicated repair method is assigned to every level of a system. This results in a hierarchical organized repair approach that combines various fault-tolerant repair methods. The developed hierarchical repair approach uses only software-based repair techniques, because the required hardware overhead for administrating a software-based repair is negligible. A permanent fault is handled by reconfiguring the application of a system in such a way that the executed tasks never use a faulty component. The reconfiguration at the core-level avoids e.g. the use of a faulty register whereas at the system-level a task is moved from a processor core to a different one. The software-based repair approach can be achieved with techniques, which are used in the back-end of a compiler. A varying set of back-ends is required for the different levels of a system. A first simple back-end adapts the scheduling of a basic block, whereas a second back-end can change the usage of registers. At the system-level a back-end is required, which adapts the program code of one core to the architecture of another core. The hierarchical repair approach is organized in such a way that a faulty core executes the software-based repair as a self-repair. In case that the self-repair fails, the repair is repeated at the system-level by an arbitrary core of the system. The thesis investigates the overhead of the software-based self-repair and the improvement of the average life-time of different fault-tolerant system configurations. KW - Zuverlässigkeit KW - Fehlertoleranz KW - Mehrkernsystem KW - Software-basierte Rekonfiguration KW - Fault-Tolerance KW - Multicore System KW - Software-based Self-Repair KW - Dependability KW - Eingebettetes System KW - Fehlertoleranz KW - Rekonfiguration Y1 - 2014 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-34916 ER - TY - THES A1 - Vörtler, Thilo T1 - Verification of software for Contiki-based low-power embedded systems using software model checking T1 - Verifikation von Anwendungen für Contiki basierende low-power eingebettete Systeme mit Hilfe von Software Model Checking N2 - The main building blocks for the internet of things are connected embedded systems. Often these systems are also used in safety critical applications. Therefore, it is particularly important that these devices work according to their specification i.e. they behave as intended. Nowadays, even for simple devices embedded operating systems as Contiki are used to simplify application development and to increase portability between different hardware platforms. The main objective of this thesis is to present a methodology for the verification of software applications written for the operation system Contiki, taking the system hardware into account. Therefore, software model checking and especially bounded model checking [BCC⁺03] is used as a technique, which allows to formally verify software for embedded systems. For verifying the software against its specification, it is also necessary to build a model of the system hardware. Thereby, the difficulty is to create a model which is detailed enough to capture the hardware behavior so that the software performs correctly, while keeping the computation effort for the verification process manageable. In this work, the drivers which communicate with the hardware are therefore replaced with abstract models during the verification process. This enables the verification based on an abstract hardware platform independent of specific hardware. A special role within embedded systems play interrupts. Interrupts are used to save power and can also be used to react on external events. Current methods for verification of interrupt driven software are based on the interleaving model and partial order reduction to reduce the size of the verification problem. This thesis argues that this method is not sufficient for software, whose behavior relies on periodically occurring interrupts. Therefore, in this thesis, a new approach called periodic interrupt modeling is introduced. This approach can be applied automatically and reduces the number of incorrect verification results due to inaccurate modeling. In addition, properties can be proven that depend on the number of occurring interrupts. Using applications for the Contiki operating system, and based on a verification flow, the approaches toward interrupt modeling are compared. N2 - Vernetzte eingebettete Systeme bilden die Grundlage für das Internet of Things (IoT). Sie arbeiten häufig autark und in sicherheitskritischen Bereichen. Deshalb ist es wichtig sicherzustellen, dass die Systeme sich korrekt, also gemäß ihrer Spezifikation, verhalten. Zur Erstellung von Software für solche Systeme werden Betriebssysteme wie Contiki verwendet, welche die Programmierung von Anwendungen vereinfachen und die Portabilität zwischen verschiedenen Hardware-Plattformen ermöglichen. In dieser Dissertation wird eine Methodik zur Verifikation von Software-Anwendungen, unter Berücksichtigung der Hardwareumgebung, für eingebettete Systeme anhand des Betriebssystems Contiki vorgestellt. Es wird die Technik des Software Model Checking [CGP00] - und dabei insbesondere Bounded Model Checking [BCC⁺03] - verwendet, welche es ermöglicht die Software eines eingebetteten Systems formal zu verifizieren. Um die Verifikation durchzuführen, muss auch die Hardware des Systems modelliert werden. Die Herausforderung hierbei ist es, die Interaktionen der Software mit der Hardware hinreichend genau abzubilden und gleichzeitig den Aufwand für die Verifikation hinsichtlich des benötigten Rechenaufwands beherrschbar zu halten. In dieser Arbeit wird deshalb ein Ansatz verwendet, der die Treiber, die auf die Hardware zu- greifen durch Softwaremodelle für die Verifikation ersetzt. Dies ermöglicht es Anwendungen für Contiki mit Hilfe einer abstrakten Verifikationsumgebung zu überprüfen. Ein besonderer Aspekt bei eingebetteten Systemen ist die Verwendung von Interrupts, welche es ermöglichen Energie, einzusparen und auf externe Ereignisse zu reagieren. In bisherigen Ansätzen zur Verifikation werden Interrupts mit dem Interleaving Modell modelliert und das Verifikationsproblem mit Hilfe von Partial Order Reduction [CGP00, BK08] reduziert. Diese Arbeit zeigt, dass dieser Ansatz für die Verifikation von Anwendungen, welche periodische Interrupts verwenden, nicht ausreichend ist. Deshalb wird mit Periodic Interrupt Modelling ein neuer Ansatz zur Modellierung von Interrupts vorgestellt. Dieser Ansatz kann automatisiert angewendet werden und verringert die Anzahl von falschen Verifikationsergebnissen aufgrund ungenauer Modellierung. Zusätzlich ist es möglich Eigenschaften zu überprüfen, die von der Häufigkeit von Interrupt-Aufrufen abhängen. Anhand des in der Arbeit entwickelten Verifikationsablaufs werden Beispielprogramme für Contiki untersucht und die Ansätze zur Interruptmodellierung verglichen. KW - Embedded Systems KW - Interrupts KW - Model Checking KW - Contiki KW - Software KW - Contiki KW - Eingebettete Systeme KW - Unterbrechungen KW - Modellprüfung KW - Software KW - Eingebettetes System KW - Interrupt KW - Bounded Model Checking KW - Software Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-44080 ER -