Shop : Verlinkung
Shop
Verlinkung
35,80 €ISBN 978-3-8440-2159-2Paperback180 Seiten50 Abbildungen267 g21 x 14,8 cmEnglischDissertation
September 2013
Neuerscheinung
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
Link zum Buch
Kopieren Sie einfach folgende Zeilen in Ihr HTML-Dokument:
Das Buch <a href="https://www.shaker.de/shop/978-3-8440-2159-2">Raimondas Sasnauskas - Symbolic Execution of Distributed Systems</a><br />(ISBN: 978-3-8440-2159-2) wurde im <a href="https://www.shaker.de">Shaker Verlag</a> veröffentlicht.
Ergebnis:
Das Buch Raimondas Sasnauskas - Symbolic Execution of Distributed Systems
(ISBN: 978-3-8440-2159-2) wurde im Shaker Verlag veröffentlicht.
(ISBN: 978-3-8440-2159-2) wurde im Shaker Verlag veröffentlicht.
Link zur Reihe
Kopieren Sie einfach folgende Zeilen in Ihr HTML-Dokument:
Die Reihe <a href="https://www.shaker.de/Reihe/533">Reports on Communications and Distributed Systems</a> erscheint im <a href="https://www.shaker.de">Shaker Verlag</a>.
Ergebnis:
Die Reihe Reports on Communications and Distributed Systems
erscheint im Shaker Verlag.
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.
