Raimondas SasnauskasSymbolic Execution of Distributed Systems | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
ISBN: | 978-3-8440-2159-2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Series: | Reports on Communications and Distributed Systems Herausgeber: Prof. Dr.-Ing. Klaus Wehrle Aachen | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Volume: | 5 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Keywords: | Symbolic Execution; Symbolic Distributed Execution; Distributed Systems; Testing Tools; Software/Program Verification | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Type of publication: | Thesis | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Language: | English | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Pages: | 180 pages | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Figures: | 50 figures | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Weight: | 267 g | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Format: | 21 x 14,8 cm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Binding: | Paperback | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Price: | 35,80 € / 44,75 SFr | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Published: | September 2013 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Buy: | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Download: | Available PDF-Files for this title: You need the Adobe Reader, to open the files. Here you get help and information, for the download. These files are not printable.
User settings for registered users You can change your address here or download your paid documents again.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Recommendation: | You want to recommend this title? | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Review copy: | Here you can order a review copy. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Link: | You want to link this page? Click here. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Export citations: |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Abstract: | 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. |