Scalable Symbolic Execution of Distributed Systems
Scalable Symbolic Execution of Distributed Systems
复制标题
DOI：
10.1109/icdcs.2011.28
复制
发表时间：
2011-06
期刊：
影响因子：
--
通讯作者：
Raimondas Sasnauskas;Oscar Soria Dustmann;Benjamin Lucien Kaminski;Klaus Wehrle;Carsten Weise;S. Kowalewski
中科院分区：
文献类型：
--
作者：
Raimondas Sasnauskas;Oscar Soria Dustmann;Benjamin Lucien Kaminski;Klaus Wehrle;Carsten Weise;S. Kowalewski
最近在符号执行方面的进展已经提出了一些有希望的解决方案来自动实现高复盖率并在测试期间探索非确定性。这种有吸引力的未经修改的软件测试技术帮助开发人员提供具体的输入和确定性的时间表，以分析错误的程序路径。这些工具能够处理复杂系统的软件，只考虑单个软件实例，而不考虑它们的分布式执行，这构成了分布式系统的核心。然而，通向符号分布式执行的这一步是陡峭的，这带来了两个核心挑战：(1)额外的状态增长和(2)通信导致的状态内部依赖。本文提出了一种支持分布式系统可扩展符号执行的新方法--SDE。我们工作的主要贡献是双重的。首先，我们对SDE的问题空间进行了泛化，并提出了一种在测试过程中显著消除冗余状态的算法。其关键思想是从节点的本地通信中受益，从而最小化代表分布式执行的状态数量。其次，我们通过三个运行Contiki操作系统的传感器网络场景验证了SDE在测试中的实际适用性。
Recent advances in symbolic execution have proposed a number of promising solutions to automatically achieve high-coverage and explore non-determinism during testing. This attractive testing technique of unmodified software assists developers with concrete inputs and deterministic schedules to analyze erroneous program paths. Being able to handle complex systems' software, these tools only consider single software instances and not their distributed execution which forms the core of distributed systems. The step to symbolic distributed execution is however steep, posing two core challenges: (1) additional state growth and (2) the state intra-dependencies resulting from communication. In this paper, we present SDE -- a novel approach enabling scalable symbolic execution of distributed systems. The key contribution of our work is two-fold. First, we generalize the problem space of SDE and develop an algorithm significantly eliminating redundant states during testing. The key idea is to benefit from the nodes' local communication minimizing the number of states representing the distributed execution. Second, we demonstrate the practical applicability of SDE in testing with three sensor net scenarios running Contiki OS.