CAREER: Towards a Unified Declarative Platform for Composable Verifiable Networks

职业：迈向可组合可验证网络的统一声明性平台

• 批准号: 0845552
• 负责人: Boon Thau Loo
• 金额: $ 45万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-06-01 至 2016-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0845552&HistoricalAwards=false
• 关键词: CAREER; Towards; Unified; Declarative; Platform

CNS - 0845552 Loo, Boon Thau University of PennsylvaniaCAREER: Towards a Unified Declarative Platform for ComposableVerifiable NetworksThis research project investigates a declarative, composable and verifiable network infrastructure -- one capable of bridging between existing networks, stacking them in layers, dynamically changing the layers or bridges, and allowing for rapid extensibility with new functionalities. The proposed infrastructure utilizes declarative networking, a declarative, database-inspired extensible infrastructure that uses query languages to specify behavior. This approach provides the benefits of compactness, safety, composability, and the potential for correctness checks.Intellectual Merit. The first contribution of the proposed research explores mechanisms for network composition where distinct parts or elements of existing networks are combined via declarative specifications to create a new network with new functionalities. The second contribution leverages the dynamic composition capabilities provided by the declarative framework and infrastructure to enable adaptable hybrid protocols, i.e. protocols built from combining several existing protocols based on changing application needs and network conditions. The third contribution explores a formal methodology towards verifying the properties of declarative networks and their compositions. Three verification techniques will be explored: static analysis of database query languages, theorem proving techniques that leverages declarative networking's connection to logic programs, and runtime verification.Broader Impact. The education goal of this proposal is an integrated research and teaching program that emphasizes data-centric and formal methods approaches towards networking. The intellectual merit of this proposal is the development of a unified declarative framework for specifying, composing, formally verifying, and implementing networks. The broader impact of this proposal lies in the ability to enable and create new functionalities from the network diversity that technologies such as virtualization and overlays make possible.

CNS - 0845552 Loo，布恩陶 University of Pennsylvania宾夕法尼亚大学可组合可验证网络的统一声明平台这个研究项目研究了一个声明性的、可组合的和可验证的网络基础设施--一个能够在现有网络之间桥接的基础设施，将它们分层堆叠，动态地改变层或桥，并允许快速扩展新功能。建议的基础设施利用声明式网络，声明式，数据库启发的可扩展的基础设施，使用查询语言来指定行为。 这种方法提供了紧凑性、安全性、可组合性和正确性检查的可能性等优点。拟议研究的第一个贡献是探索网络组合机制，通过声明性规范将现有网络的不同部分或元素组合在一起，以创建具有新功能的新网络。 第二个贡献是利用声明性框架和基础设施提供的动态组合能力，以实现可适应的混合协议，即基于不断变化的应用需求和网络条件组合几个现有协议而构建的协议。 第三个贡献探索了验证声明性网络及其组成的属性的正式方法。本课程将探讨三种验证技术：数据库查询语言的静态分析、利用声明式网络与逻辑程序的连接的定理证明技术，以及运行时验证。该提案的教育目标是一个综合的研究和教学计划，强调以数据为中心的正式方法，实现网络。这个建议的智力价值是开发一个统一的声明性框架，用于指定，组成，正式验证和实现网络。 该提案的更广泛影响在于能够从虚拟化和覆盖等技术所实现的网络多样性中启用和创建新功能。