Shop : Details
Shop
Details
35,80 €ISBN 978-3-8440-2159-2Softcover180 pages50 figures267 g21 x 14,8 cmEnglishThesis
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.
Keywords: Symbolic Execution; Symbolic Distributed Execution; Distributed Systems; Testing Tools; Software/Program Verification
Reports on Communications and Distributed Systems
Edited by Prof. Dr.-Ing. Klaus Wehrle, Aachen
Volume 5
Available online documents for this title
You need Adobe Reader, to view these files. Here you will find a little help and information for downloading the PDF files.
Please note that the online documents cannot be printed or edited.
Please also see further information at: Help and Information.
Please also see further information at: Help and Information.
| Document |  | Document | ||
| Type |  | |||
| Costs |  | 26,85 € | ||
| Action |  | Purchase in obligation and download the file | ||
| Document |  | Table of contents | ||
| Type | | |||
| Costs |  | free | ||
| Action |  | Download the file | ||
User settings for registered online customers (online documents)
You can change your address details here and access documents you have already ordered.
User
Not logged in
Export of bibliographic data
Shaker Verlag GmbH
Am Langen Graben 15a
52353 Düren
Germany
Am Langen Graben 15a
52353 Düren
Germany
Mon. - Thurs. 8:00 a.m. to 4:00 p.m.
Fri. 8:00 a.m. to 3:00 p.m.
Fri. 8:00 a.m. to 3:00 p.m.
Contact us. We will be happy to help you.
