Abstractions that Simplify the Design and Verification of Fault-Tolerant Distributed Protocols

该研究开发了简化设计的技术， 分布式计算容错协议的验证 系统. 协议设计者提供了一个虚拟 系统具有完美的处理器同步，可靠的通信， 和简单的处理器故障。 为此虚拟机编写的协议 系统被转换成在“真实的”中正确运行的协议 处理器不同步、通信不可靠的系统，以及 更复杂的故障。 这种方法使设计师避免了 底层系统复杂性的几个方面;协议 设计并验证了较简单的虚拟系统，然后运行 在更复杂的底层系统中进行仿真。

The research develops techniques that simplify the design and verification of fault-tolerant protocols for distributed computing systems. Protocol designers provided with the abstraction of a virtual system with perfect processor synchronization, reliable communication, and simple processor failures. Protocols written for this virtual system are translated into protocols that run correctly in "real" systems with unsynchronized processors, unreliable communication, and more complex failures. This methodology shields the designer from several aspects of the underlying system complexity; protocols are designed and verified for the simpler virtual system, and then run by simulation in the more complex underlying system.