Compositional programming and testing of dynamic distributed systems
Compositional programming and testing of dynamic distributed systems
复制标题
动态分布式系统的组合编程和测试
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
S. Seshia
中科院分区：
文献类型：
--
作者：
Ankush Desai;Amar Phanishayee;S. Qadeer;S. Seshia
现实世界的分布式系统很少以独立的整体系统实现。相反，它由多个独立的交互组件组成，这些组件共同确保所需的系统级规范。通过将系统级测试问题分解为简单组件级测试问题的集合，可以将系统测试扩展到大型工业规模的实现。本文提出了针对分布式系统的组成编程和具有两个核心贡献的分布式系统的技术：（1）我们根据组合物跟踪改进的理论提出了一个模块系统，用于动态系统的组合痕量改进理论，该系统由异步沟通的状态机器组成，可以在其中动态机器动态地进行动态机器。创建的现有状态机器的通信拓扑可以在运行时更改； （2）我们提出了MODP，这是一种实现我们的模块系统以实现分布式系统的组成推理（假设）的编程系统。我们通过构建两个实用的耐故障分布式系统，一项交易仪式服务和一个复制的哈希表来证明框架的功效。 MODP有助于模块化实现这些系统，并通过组成测试验证它们。我们从经验上证明，基于抽象的组成推理方法有助于放大测试过程中的覆盖范围，并将其扩展到现实世界分布式系统。使用MODP构建的分布式服务实现了与开源等效物相当的性能。
A real-world distributed system is rarely implemented as a standalone monolithic system. Instead, it is composed of multiple independent interacting components that together ensure the desired system-level specification. One can scale systematic testing to large, industrial-scale implementations by decomposing the system-level testing problem into a collection of simpler component-level testing problems. This paper proposes techniques for compositional programming and testing of distributed systems with two central contributions: (1) We propose a module system based on the theory of compositional trace refinement for dynamic systems consisting of asynchronously-communicating state machines, where state machines can be dynamically created, and communication topology of the existing state machines can change at runtime; (2) We present ModP, a programming system that implements our module system to enable compositional reasoning (assume-guarantee) of distributed systems. We demonstrate the efficacy of our framework by building two practical fault-tolerant distributed systems, a transaction-commit service and a replicated hash-table. ModP helps implement these systems modularly and validate them via compositional testing. We empirically demonstrate that the abstraction-based compositional reasoning approach helps amplify the coverage during testing and scale it to real-world distributed systems. The distributed services built using ModP achieve performance comparable to open-source equivalents.
影响因子：
--
作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
通讯作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock