TY - THES A1 - Liu, Ke T1 - Parallel constraint solving for combinatorial problems T1 - Paralleles Constraint Solving für kombinatorische Probleme N2 - With parallelism becoming the standard in computer design, research on parallel constraint solving technique is of vital importance for enhancing the performance of constraint solving. In this dissertation, we reviewed the literature on exploiting parallelism in constraint solving to help gain insight into the rationale of different types of parallel constraint solving approaches. On this basis, we analyzed the effectiveness of parallel constraint solving, with the focus on obtaining a first solution when solving computationally hard combinatorial problems. We have shown that a well-designed search space splitting method and constraint programming model can enable the embarrassingly parallel search (EPS) to solve some open instances of the social golfer problem that have not been solved by a sequential algorithm. We also observed superlinear speedups when solving these instances, which confirms our theoretical analysis. Besides, we examined two practical constraint optimization problems, including the traveling tournament problem with predefined venues and the talent scheduling problem. Our proposed constraint models outperformed the existing models on the same instances, and the EPS approach could always attain better feasible solutions in terms of the optimal objective value by using more parallel processors. To explore the use of massively parallel processing, we proposed the parallel stochastic portfolio search, which is a simple and non-intrusive way to parallelize different incarnations of a sequential solver. When comparing the existing portfolio to our portfolio approach by solving the same constraint satisfaction problems using the same constraint models, our technique could solve harder and larger instances. The successes of our new parallel approaches are attributed to early diversity; i.e., some diversity early in the search introduced by parallelism can offset early mistakes caused by weak heuristic choices. Unlike the other techniques (e.g., limited discrepancy search) used to overcome early mistakes, the studied two parallel constraint solving approaches not only can explore more nodes simultaneously but also does not sacrifice the guarantee of completeness. We also presented a hypertree decomposition method that builds a degenerate decomposition tree for a given constraint network, in which each node of the decomposition tree possesses and executes a subset of constraints of the given constraint network. The usefulness of our proposed parallel techniquedepends on whether we can find an efficient way to join the results of each node. N2 - Da Parallelität zum Standard im Computerdesign geworden ist, ist die Erforschung paralleler Constraint-Solving-Techniken von entscheidender Bedeutung, um die Leistung des Constraint-Solving zu verbessern. In dieser Dissertation wurde die Literatur zur Ausnutzung der Parallelität bei der Lösung von Nebenbedingungen durchgesehen, um einen Einblick in die Gründe für die verschiedenen Arten von parallelen Lösungsansätzen für Nebenbedingungen zu erhalten. Auf dieser Grundlage haben wir die Effektivität des parallelen Lösens von Nebenbedingungen analysiert, wobei der Schwerpunkt auf der Erlangung einer ersten Lösung beim Lösen rechenintensiver kombinatorischer Probleme lag. Wir haben gezeigt, dass eine gut konzipierte Suchraumaufteilungsmethode und ein Constraint-Programmiermodell die peinlich parallele Suche (EPS) in die Lage versetzen kann, einige offene Instanzen des sozialen Golferproblems zu lösen, die von einem sequentiellen Algorithmus nicht gelöst werden konnten. Wir beobachteten auch superlineare Beschleunigungen beim Lösen dieser Instanzen, was unsere theoretische Analyse bestätigt. Außerdem untersuchten wir zwei praktische Constraint-Optimierungsprobleme, darunter das Traveling-Turnier-Problem mit vordefinierten Austragungsorten und das Talentplanungsproblem. Die von uns vorgeschlagenen Constraint-Modelle übertrafen die bestehenden Modelle bei denselben Instanzen, und der EPS-Ansatz konnte durch die Verwendung von mehr parallelen Prozessoren immer bessere machbare Lösungen in Bezug auf den optimalen Zielwert erzielen. Um die Verwendung von massiv paralleler Verarbeitung zu erforschen, haben wir die parallele stochastische Portfoliosuche vorgeschlagen, die eine einfache und nicht-intrusive Methode zur Parallelisierung verschiedener Inkarnationen eines sequentiellen Solvers ist. Beim Vergleich des existierenden Portfolios mit unserem Portfolio-Ansatz durch Lösen der gleichen Constraint-Satisfaction-Probleme unter Verwendung der gleichen Constraint-Modelle konnte unsere Technik schwierigere und größere Instanzen lösen. Die Erfolge unserer neuen parallelen Ansätze werden auf die frühe Diversität zurückgeführt, d. h. eine gewisse Diversität zu Beginn der Suche, die durch die Parallelität eingeführt wird, kann frühe Fehler ausgleichen, die durch schwache heuristische Entscheidungen verursacht werden. Im Gegensatz zu anderen Techniken (z. B. begrenzte Diskrepanzsuche), die zur Überwindung früher Fehler verwendet werden, können die beiden untersuchten parallelen Ansätze zum Lösen von Beschränkungen nicht nur mehr Knoten gleichzeitig untersuchen, sondern opfern auch nicht die Garantie der Vollständigkeit. Wir haben auch eine Hypertree-Dekompositionsmethode vorgestellt, die einen degenerierten Dekompositionsbaum für ein gegebenes Constraint-Netzwerk aufbaut, bei dem jeder Knoten des Dekompositionsbaums eine Teilmenge von Constraints des gegebenen Constraint-Netzwerks besitzt und ausführt. Die Nützlichkeit der von uns vorgeschlagenen parallelen Technik hängt davon ab, ob wir einen effizienten Weg finden können, die Ergebnisse der einzelnen Knoten zu verbinden. KW - Parallel constraint solving KW - Parallel computing KW - Constraint programing KW - Constraint-Programmierung KW - Lösen von Zwangsbedingungen KW - Paralleles Rechnen KW - SGP KW - Constraint-Programmierung KW - Parallelverarbeitung Y1 - 2021 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-54375 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 - TY - THES A1 - Liu, Ke T1 - Parallel constraint solving for combinatorial problems T1 - Paralleles Constraint Solving für kombinatorische Probleme N2 - With parallelism becoming the standard in computer design, research on parallel constraint solving technique is of vital importance for enhancing the performance of constraint solving. In this dissertation, we reviewed the literature on exploiting parallelism in constraint solving to help gain insight into the rationale of different types of parallel constraint solving approaches. On this basis, we analyzed the effectiveness of parallel constraint solving, with the focus on obtaining a first solution when solving computationally hard combinatorial problems. We have shown that a well-designed search space splitting method and constraint programming model can enable the embarrassingly parallel search (EPS) to solve some open instances of the social golfer problem that have not been solved by a sequential algorithm. We also observed superlinear speedups when solving these instances, which confirms our theoretical analysis. Besides, we examined two practical constraint optimization problems, including the traveling tournament problem with predefined venues and the talent scheduling problem. Our proposed constraint models outperformed the existing models on the same instances, and the EPS approach could always attain better feasible solutions in terms of the optimal objective value by using more parallel processors. To explore the use of massively parallel processing, we proposed the parallel stochastic portfolio search, which is a simple and non-intrusive way to parallelize different incarnations of a sequential solver. When comparing the existing portfolio to our portfolio approach by solving the same constraint satisfaction problems using the same constraint models, our technique could solve harder and larger instances. The successes of our new parallel approaches are attributed to early diversity; i.e., some diversity early in the search introduced by parallelism can offset early mistakes caused by weak heuristic choices. Unlike the other techniques (e.g., limited discrepancy search) used to overcome early mistakes, the studied two parallel constraint solving approaches not only can explore more nodes simultaneously but also does not sacrifice the guarantee of completeness. We also presented a hypertree decomposition method that builds a degenerate decomposition tree for a given constraint network, in which each node of the decomposition tree possesses and executes a subset of constraints of the given constraint network. The usefulness of our proposed parallel techniquedepends on whether we can find an efficient way to join the results of each node. N2 - Da Parallelität zum Standard im Computerdesign geworden ist, ist die Erforschung paralleler Constraint-Solving-Techniken von entscheidender Bedeutung, um die Leistung des Constraint-Solving zu verbessern. In dieser Dissertation wurde die Literatur zur Ausnutzung der Parallelität bei der Lösung von Nebenbedingungen durchgesehen, um einen Einblick in die Gründe für die verschiedenen Arten von parallelen Lösungsansätzen für Nebenbedingungen zu erhalten. Auf dieser Grundlage haben wir die Effektivität des parallelen Lösens von Nebenbedingungen analysiert, wobei der Schwerpunkt auf der Erlangung einer ersten Lösung beim Lösen rechenintensiver kombinatorischer Probleme lag. Wir haben gezeigt, dass eine gut konzipierte Suchraumaufteilungsmethode und ein Constraint-Programmiermodell die peinlich parallele Suche (EPS) in die Lage versetzen kann, einige offene Instanzen des sozialen Golferproblems zu lösen, die von einem sequentiellen Algorithmus nicht gelöst werden konnten. Wir beobachteten auch superlineare Beschleunigungen beim Lösen dieser Instanzen, was unsere theoretische Analyse bestätigt. Außerdem untersuchten wir zwei praktische Constraint-Optimierungsprobleme, darunter das Traveling-Turnier-Problem mit vordefinierten Austragungsorten und das Talentplanungsproblem. Die von uns vorgeschlagenen Constraint-Modelle übertrafen die bestehenden Modelle bei denselben Instanzen, und der EPS-Ansatz konnte durch die Verwendung von mehr parallelen Prozessoren immer bessere machbare Lösungen in Bezug auf den optimalen Zielwert erzielen. Um die Verwendung von massiv paralleler Verarbeitung zu erforschen, haben wir die parallele stochastische Portfoliosuche vorgeschlagen, die eine einfache und nicht-intrusive Methode zur Parallelisierung verschiedener Inkarnationen eines sequentiellen Solvers ist. Beim Vergleich des existierenden Portfolios mit unserem Portfolio-Ansatz durch Lösen der gleichen Constraint-Satisfaction-Probleme unter Verwendung der gleichen Constraint-Modelle konnte unsere Technik schwierigere und größere Instanzen lösen. Die Erfolge unserer neuen parallelen Ansätze werden auf die frühe Diversität zurückgeführt, d. h. eine gewisse Diversität zu Beginn der Suche, die durch die Parallelität eingeführt wird, kann frühe Fehler ausgleichen, die durch schwache heuristische Entscheidungen verursacht werden. Im Gegensatz zu anderen Techniken (z. B. begrenzte Diskrepanzsuche), die zur Überwindung früher Fehler verwendet werden, können die beiden untersuchten parallelen Ansätze zum Lösen von Beschränkungen nicht nur mehr Knoten gleichzeitig untersuchen, sondern opfern auch nicht die Garantie der Vollständigkeit. Wir haben auch eine Hypertree-Dekompositionsmethode vorgestellt, die einen degenerierten Dekompositionsbaum für ein gegebenes Constraint-Netzwerk aufbaut, bei dem jeder Knoten des Dekompositionsbaums eine Teilmenge von Constraints des gegebenen Constraint-Netzwerks besitzt und ausführt. Die Nützlichkeit der von uns vorgeschlagenen parallelen Technik hängt davon ab, ob wir einen effizienten Weg finden können, die Ergebnisse der einzelnen Knoten zu verbinden. KW - Parallel constraint solving KW - Parallel computing KW - Constraint programing KW - Constraint-Programmierung KW - Lösen von Zwangsbedingungen KW - Paralleles Rechnen KW - SGP KW - Constraint-Programmierung KW - Parallelverarbeitung Y1 - 2021 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-53999 ER -