@phdthesis{Mueller2014, author = {M{\"u}ller, Sebastian}, title = {Software-basierte Rekonfiguration in statisch geplanten Mehrkernsystemen zur Behandlung permanenter Fehler}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-34916}, school = {BTU Cottbus - Senftenberg}, year = {2014}, abstract = {In zuk{\"u}nftigen eingebetteten Systemen ist bei zunehmender Integrationsdichte mit einer abnehmenden Zuverl{\"a}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{\"u}chtigkeit solcher Systeme auch f{\"u}r einen langen Zeitraum zu gew{\"a}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{\"u}r bereits verschiedene Ans{\"a}tze auf unterschiedlichen Systemebenen. Das Spektrum solcher Ans{\"a}tze reicht von einer Reparatur auf Transistorebene {\"u}ber die Reparatur einzelner Komponenten, die aus einigen dutzend bis einigen tausend Transistoren bestehen, bis hin zu Reparaturans{\"a}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{\"a}t wird jedoch ein hierarchischer Ansatz ben{\"o}tigt, der die existierenden Techniken ebenen{\"u}bergreifend verbindet. Dadurch kann eine Zerlegung des Systems in verschiedene Gruppen vorgenommen werden, wobei f{\"u}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{\"u}r das hierarchische Verfahren insbesondere software-basierte Reparaturans{\"a}tze betrachtet, da diese nur einen geringen Administrationsaufwand in Hardware erfordern. Die Nutzung fehlerhafter Komponenten im Prozessor wird dabei durch die Anpassung des ausgef{\"u}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{\"a}chtige Backends. Das reicht von einem Backend, das nur eine Ablaufplanung {\"a}ndert, {\"u}ber ein Backend, das dar{\"u}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{\"u}hrung der software-basierten Reparatur soll dabei m{\"o}glichst durch den fehlerhaften Kern selbst ausgef{\"u}hrt werden. In schwerwiegenden F{\"a}llen erfolgt eine administrierte Reparatur auf der Systemebene durch einen zur Reparaturzeit bestimmten Prozessorkern des Systems. Der Aufwand f{\"u}r entsprechende Backends sowie deren M{\"o}glichkeit zur Fehlerbehandlung werden in dieser Arbeit untersucht.}, subject = {Zuverl{\"a}ssigkeit; Fehlertoleranz; Mehrkernsystem; Software-basierte Rekonfiguration; Fault-Tolerance; Multicore System; Software-based Self-Repair; Dependability; Eingebettetes System; Fehlertoleranz; Rekonfiguration}, language = {de} } @phdthesis{Voertler2017, author = {V{\"o}rtler, Thilo}, title = {Verification of software for Contiki-based low-power embedded systems using software model checking}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-44080}, school = {BTU Cottbus - Senftenberg}, year = {2017}, abstract = {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.}, subject = {Embedded Systems; Interrupts; Model Checking; Contiki; Software; Contiki; Eingebettete Systeme; Unterbrechungen; Modellpr{\"u}fung; Software; Eingebettetes System; Interrupt ; Bounded Model Checking; Software}, language = {en} }