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

SHF：小：协作研究：网络更新的实际综合

• 批准号: 1421752
• 负责人: Pavol Cerny
• 金额: $ 24.65万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-01 至 2018-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1421752&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Practical

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.

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