Shop : Details
Shop
Details
35,80 €ISBN 978-3-8440-2159-2Paperback180 Seiten50 Abbildungen267 g21 x 14,8 cmEnglischDissertation
September 2013
Raimondas Sasnauskas
Symbolic Execution of Distributed Systems
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.
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.
Schlagwörter: Symbolic Execution; Symbolic Distributed Execution; Distributed Systems; Testing Tools; Software/Program Verification
Reports on Communications and Distributed Systems
Herausgegeben von Prof. Dr.-Ing. Klaus Wehrle, Aachen
Band 5
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.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
| Dokument |  | Gesamtdokument | ||
| Dateiart |  | |||
| Kosten |  | 26,85 € | ||
| Aktion |  | Zahlungspflichtig kaufen und download der Datei | ||
| Dokument |  | Inhaltsverzeichnis | ||
| Dateiart | | |||
| Kosten |  | frei | ||
| Aktion |  | Download der Datei | ||
Benutzereinstellungen für registrierte Online-Kunden (Online-Dokumente)
Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
Benutzer
Nicht angemeldet
Export bibliographischer Daten
Shaker Verlag GmbH
Am Langen Graben 15a
52353 Düren
Am Langen Graben 15a
52353 Düren
Mo. - Do. 8:00 Uhr bis 16:00 Uhr
Fr. 8:00 Uhr bis 15:00 Uhr
Fr. 8:00 Uhr bis 15:00 Uhr
Kontaktieren Sie uns. Wir helfen Ihnen gerne weiter.
