Raimondas SasnauskasSymbolic Execution of Distributed Systems | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
ISBN: | 978-3-8440-2159-2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Reihe: | Reports on Communications and Distributed Systems Herausgeber: Prof. Dr.-Ing. Klaus Wehrle Aachen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Band: | 5 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Schlagwörter: | Symbolic Execution; Symbolic Distributed Execution; Distributed Systems; Testing Tools; Software/Program Verification | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Publikationsart: | Dissertation | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Sprache: | Englisch | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Seiten: | 180 Seiten | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Abbildungen: | 50 Abbildungen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Gewicht: | 267 g | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Format: | 21 x 14,8 cm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Bindung: | Paperback | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Preis: | 35,80 € | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Erscheinungsdatum: | September 2013 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Kaufen: | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Download: | Verfügbare Online-Dokumente zu diesem Titel: Sie benötigen den Adobe Reader, um diese Dateien ansehen zu können. Hier erhalten Sie eine kleine Hilfe und Informationen, zum Download der PDF-Dateien. Bitte beachten Sie, dass die Online-Dokumente nicht ausdruckbar und nicht editierbar sind.
Benutzereinstellungen für registrierte Online-Kunden Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Weiterempfehlung: | Sie möchten diesen Titel weiterempfehlen? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Rezensionsexemplar: | Hier können Sie ein Rezensionsexemplar bestellen. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Verlinken: | Sie möchten diese Seite verlinken? Hier klicken. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Export Zitat: |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Zusammenfassung: | Automatism and high code coverage are the core challenges in testing distributed systems in their early development phase. Ideally, the testing process should cope with a large input space, non-determinism, concurrency, and heterogeneous operating environments to effectively explore the behavior of unmodified software. In practice, however, missing tool support imposes significant manual effort to perform high-coverage and integrated testing. One of the main testing challenges is to detect bugs that occur due to unexpected inputs or non-deterministic events such as node reboots or packet duplicates, to name a few. Often, these events have the potential to drive distributed systems into corner case situations, exhibiting bugs that are hard to detect using established testing and debugging techniques. Recent advances in symbolic execution have proposed a number of effective solutions to automatically achieve high code coverage and detect bugs during testing of sequential, non-distributed programs. This attractive testing technique of unmodified code assists developers with concrete inputs to analyze distinct program paths. Being able to handle complex systems' software, these approaches only consider sequential programs and not their concurrent and distributed execution. In this thesis, we present symbolic distributed execution (SDE) -- a novel approach enabling symbolic execution of distributed systems. The main contribution of our work is three-fold. First, we generalize the problem space of SDE and develop methods to enhance symbolic execution for distributed software analysis. Second, we significantly optimize the basic execution model of SDE by eliminating redundant execution paths. The key idea is to benefit from the nodes' local communication and, thus, to minimize the number of states that represent a distributed execution. Third, we demonstrate the practical applicability of SDE with our tools KleeNet and SymNet, which are implemented as modular extensions of two popular symbolic execution frameworks. With KleeNet, we realize an automated testing environment for self-contained distributed systems that generates test cases at high code coverage, including low-probability corner case situations before deployment. As a case study, we apply KleeNet to the Contiki operating system and show its effectiveness by detecting four insidious bugs in the uIP protocol stack. One of these bugs is critical and lead to the refusal of further TCP connections. Our second tool called SymNet provides a testing environment for unmodified software running in virtual machines that communicate in a real network setup. We combine time synchronization of virtual machines and constraint synchronization to explore distinct distributed execution paths. The application of our SymNet prototype to a HIP protocol implementation exposed a design bug and thereby demonstrates SymNet's effectiveness in automated testing of complex communication software. |