Towards Verified Self-Driving Infrastructure
Towards Verified Self-Driving Infrastructure
复制标题
迈向经过验证的自动驾驶基础设施
DOI：
10.1145/3422604.3425949
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Brighten Godfrey
中科院分区：
文献类型：
--
作者：
Bingzhe Liu;A. Kheradmand;M. Caesar;Brighten Godfrey
现代“自动驾驶”服务基础设施由各种分布式控制组件组成，提供广泛的以应用程序和网络为中心的功能。这些交互的复杂性和不确定性导致故障，从细微的灰色故障到灾难性的服务中断，这些故障很难预测和修复。我们的目标是提醒人们注意对动态服务基础设施控制的正式理解的必要性。我们概述了大型服务提供商报告的几个事件以及流行的编排系统中的问题，确定了系统的关键特征及其故障。然后，我们提出了一种验证方法，其中我们将控制组件和环境的抽象模型视为参数转换系统，并利用符号模型检查来验证安全性和活动性属性，或提出安全配置参数。我们的初步实验表明，我们的方法在分析具有可接受性能开销的复杂故障场景时是有效的。
Modern "self-driving'' service infrastructures consist of a diverse collection of distributed control components providing a broad spectrum of application- and network-centric functions. The complex and non-deterministic nature of these interactions leads to failures, ranging from subtle gray failures to catastrophic service outages, that are difficult to anticipate and repair. Our goal is to call attention to the need for formal understanding of dynamic service infrastructure control. We provide an overview of several incidents reported by large service providers as well as issues in a popular orchestration system, identifying key characteristics of the systems and their failures. We then propose a verification approach in which we treat abstract models of control components and the environment as parametric transition systems and leverage symbolic model checking to verify safety and liveness properties, or propose safe configuration parameters. Our preliminary experiments show that our approach is effective in analyzing complex failure scenarios with acceptable performance overhead.
检测分布式控制平面的网络负载违规
DOI：
10.1145/3385412.3385976
发表时间：
2020
期刊：
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
影响因子：
--
作者：
Subramanian, Kausik;Abhashkumar, Anubhavnidhi;D'Antoni, Loris;Akella, Aditya
通讯作者：
Akella, Aditya
Tiramisu：快速多层网络验证
DOI：
--
发表时间：
2020
期刊：
17th USENIX Symposium on Networked Systems Design and Implementation
影响因子：
--
作者：
Abhashkumar, A.;Gember-Jacobson, A.;Akella, A.
通讯作者：
Akella, A.
Bayonet：网络概率推理
DOI：
10.1145/3192366.3192400
发表时间：
2018
期刊：
PLDI 2018 Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Gehr, Timon;Misailovic, Sasa;Tsankov, Petar;Vanbever, Laurent;Wiesmann, Pascal;Vechev, Martin
通讯作者：
Vechev, Martin