一句话：提出 TLC 时序程序逻辑，通过降低组件规约支持分布式组件栈的组合式安全性与活性验证，并证明其可靠性。
分布式系统通常由分层网络中间件组件栈构建，复杂且易出错。本文提出 TLC（Temporal Logic of Components），一种面向分布式组件的时序程序逻辑，提供直观的推理规则以验证组件功能实现的安全性与活性性质。为支持组合式推理，作者定义断言语言上的 lowering 变换，将组件规约降为可被子组件使用的规约。基于部分同步网络下组合组件栈的操作语义，证明 TLC 及 lowering 变换的可靠性。最后将 TLC 应用于组合并验证由基础分布式组件构成的栈，表明其可实际支持组合式验证。
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To 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 a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
@article{GriffinLSY20,
title = {TLC: temporal logic of distributed components},
author = {Jeremiah Griffin and Mohsen Lesani and Narges Shadab and Xizhe Yin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3409005}
}