CAREER: Verifying Distributed System Implementations

每天有数十亿人依赖分布式系统来获得医疗保健、银行、交通等服务。 尽管进行了昂贵的测试，但这些复杂的服务在实践中仍然失败，导致数据丢失和重大服务中断，威胁到每个人的便利性，财务和安全。该项目正在开发必要的工具和技术，以验证（数学证明）在网络和机器错误行为的任何组合下分布式系统实现的安全性和可靠性。智力的优点是开发组合验证技术，程序员可以独立地证明应用程序的正确性和容错组件的可靠性。更广泛的意义和重要性是为社会所依赖的核心计算基础设施提供严格的可靠性保证，并培养新一代的工程师，他们将创建高性能，验证分布式系统implementation.This项目的目的是使验证易于处理的开发验证系统transformers自动包装简单的系统与容错机制，保证保持等价性。这种方法将对应用程序正确性的关注与容错分离开来，从而简化了证明工作，并实现了更高的代码重用。行业从业者已经在使用早期原型验证系统Transformer作为探索设计和替代实现的指南。该项目的一个成果是一个广泛的此类变压器库，涵盖了广泛的关键分布式系统功能，包括重新配置、环维护和软件更新。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Billions of people depend on distributed systems every day for health care, banking, transportation, and more. Despite costly testing efforts, these complex services still fail in practice, leading to data loss and major service outages that threaten everyone's convenience, finances, and safety. This project is developing the tools and techniques necessary to verify (mathematically prove) safety and reliability for distributed systems implementations under any combination of network and machine misbehaviors. The intellectual merits are to develop compositional verification techniques where the programmer can independently prove correctness for applications and reliability for fault-tolerance components. The broader significance and importance are to provide rigorous reliability guarantees for the core computational infrastructure society depends on and to train a new generation of engineers who will create high-performance, verified distributed systems implementations.This project aims to make verification tractable by developing verified system transformers which automatically wrap simple systems with fault tolerance mechanisms guaranteed to preserve equivalence. This approach separates concerns of application correctness from fault tolerance which eases proof effort and enables greater code reuse. Industrial practitioners are already using an early prototype verified system transformer as a guide in exploring designs and alternate implementations. An outcome of this project is an extensive library of such transformers covering a broad range of critical distributed system features including reconfiguration, ring maintenance, and software update.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.