SHF:Small:Collaborative Research:Practical Synthesis of Network Updates

配置更新是当今网络不稳定的常见来源，经常导致中断、中断甚至安全漏洞。使更新难以实现的一个关键因素是网络是具有许多相互作用组件的复杂系统。典型的数据中心网络由数千台设备组成，这对网络管理员来说是一个重大挑战，因为这些设备中的每一台都必须在更新后重新配置。本研究的目标是开发使用基于软件合成的技术实现网络配置更新的新机制。为了实现这一目标，该研究正在开发(i)基于高效增量模型检查技术的新合成算法；（ii）使用定量约束和目标函数对带宽和容错建模的扩展；（三）基于并发和分布式编程连接的理论基础。该项目将会产生广泛的影响，因为它将发现新的技术，使困难的网络管理任务自动化，并通过训练本科生和研究生在正式方法和网络方面的跨学科技能。

Configuration updates are a common source of instability in networkstoday, frequently leading to outages, disruptions, and even securityvulnerabilities. A key factor that makes updates difficult toimplement is that networks are complex systems with many interactingcomponents. A typical datacenter network consists ofthousands of devices, a significant challenge for network administratorsis that each of these devices must be reconfigured after an update. The goal of this research is to develop new mechanisms for implementing network configuration updates using techniques based on software synthesis. To meet this goal, the research is developing (i) new synthesisalgorithms based on efficient incremental model checking techniques;(ii) extensions that model bandwidth and fault tolerance usingquantitative constraints and objective functions; and (iii)theoretical foundations based on connections to concurrent anddistributed programming. The project will have broad impact bydiscovering new techniques that automate a difficult networkadministration task and by training undergraduate and graduatestudents with interdisciplinary skills in formal methods andnetworking.