论文标题
分布式算法和系统的保证：安全性和livese的运行时检查
Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness
论文作者
论文摘要
本文介绍了一种通用框架和方法，用于在高级语言中（如伪模式语言）完成分布式算法的完整编程和检查分布式算法，但分别是正式规格语言和实用的编程语言，但可以精确地指定和直接执行。检查框架以及分布式算法的编写及其安全性和LIVISE属性的规范，使用distalgo，distalgo，一种用于分布式算法的高级语言。我们为检查框架提供了完整的可执行规范，并提供了完整的示例算法和示例安全性和LIVISE属性。
This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.
