TLC: temporal logic of distributed components
TLC: temporal logic of distributed components
复制标题
TLC：分布式组件的时序逻辑
DOI：
10.1145/3409005
复制
发表时间：
2020
影响因子：
--
通讯作者：
Yin, Xizhe
中科院分区：
文献类型：
--
作者：
Griffin, Jeremiah;Lesani, Mohsen;Shadab, Narges;Yin, Xizhe
分布式系统对于可靠和可扩展的计算至关重要；然而，它们本质上很复杂并且容易出现错误。为了管理这种复杂性，网络中间件传统上构建在分层的组件堆栈中。我们提出了一种分布式堆栈组合验证的新颖方法，仅基于较低组件的规范来验证每个组件。我们提出了 TLC（组件时态逻辑），这是一种新颖的时态程序逻辑，它提供直观的推理规则，用于验证分布式组件功能实现的安全性和活跃性属性。为了支持组合推理，我们在断言语言上定义了一种新颖的转换，它降低了用作子组件的组件的规范。我们证明了 TLC 的可靠性以及针对部分同步网络中组合组件堆栈的新颖操作语义的降低变换。我们成功地应用 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.
登录
查看更多内容
DOI：
10.1145/1731060.1731062
发表时间：
2009-04
期刊：
--
影响因子：
--
作者：
M. Yabandeh;N. Knežević;Dejan Kostic;Viktor Kunčak
通讯作者：
M. Yabandeh;N. Knežević;Dejan Kostic;Viktor Kunčak
DOI：
--
发表时间：
2003
期刊：
--
影响因子：
--
作者：
R. Boichat;P. Dutta;Svend Frølund;R. Guerraoui
通讯作者：
R. Boichat;P. Dutta;Svend Frølund;R. Guerraoui
DOI：
10.1145/2384616.2384645
发表时间：
2012
期刊：
2016 IEEE Frontiers in Education Conference (FIE)
影响因子：
--
作者：
Yanhong A. Liu;S. Stoller;Bo Lin;Michael Gorbovitski
通讯作者：
Michael Gorbovitski
影响因子：
--
作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
通讯作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
DOI：
10.1145/2986012.2986014
发表时间：
2016-10
期刊：
Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
影响因子：
--
作者：
Heather Miller;Philipp Haller;N. Müller;Jocelyn Boullier
通讯作者：
Heather Miller;Philipp Haller;N. Müller;Jocelyn Boullier