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

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

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.