论文标题
合并分布式组件的时间逻辑
Temporal Logic of Composable Distributed Components
论文作者
论文摘要
分布式系统对于可靠且可扩展的计算至关重要；但是，它们本质上很复杂，容易出现虫子。为了模块化管理这种复杂性，网络中间件传统上是在组件的分层堆栈中构建的。我们提出了一种新的方法来对分布式堆栈的组成验证，以仅根据较低组件的规范来验证每个组件。我们提出了TLC（组件的时间逻辑），这是一种新型的时间程序逻辑，它为验证分布式组件功能实现的安全性和LIVISE属性提供了直观的推理规则。为了支持组成推理，我们在断言语言上定义了一种新的变换，该转换降低了要用作子组件的组件的规范。我们证明了TLC的合理性和相对于分布式组件堆栈的操作语义的降低转换。我们成功地使用TLC来组成和验证一堆基本分布式组件。
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To modularly manage this complexity, network middleware has been traditionally built in layered stacks of components. We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to the operational semantics for stacks of distributed components. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
