FMitF: Track I: ComScaN: Composition and Scaling of Network Service Functions

在当今互联的世界中，网络运营商需要能够按需快速部署、更新和扩展服务。构建这样的系统是具有挑战性的，并且确保其正确性和性能一直是难以捉摸的。该项目团队旨在开发一种“绿色领域”方法，以支持未来的网络和新兴服务，其方式是可扩展性是设计所固有的，正确性和性能要求可以用数学严谨性来支持。这是通过汇集和扩展网络系统，编程语言和软件验证方法领域的最新研究进展来实现的。这旨在为网络运营商提供表达各种服务的期望要求的能力，轻松调整这些服务以跟上不断变化的需求和不断发展的网络基础设施的灵活性，以及维护性能和正确性目标的保证。这项研究预计将产生一个可行的原型，展示核心思想沿着一个生态系统的开源软件工具，实验数据和示例应用程序。从该项目中学到的知识将被纳入学术课程，以使劳动力具备构建可靠且高性能的网络基础设施所需的技能。这项工作是通过吸引、吸引和指导一群不同的初露头角的研究人员来进行的，目的是欢迎和鼓励迄今为止代表性不足的群体参与先进的计算研究。在这个项目中，主要研究人员提出了一种绿色领域的方法，以实现网络功能虚拟化（NFV）扩展的定量性能推理。它是基于正式的基础和原则性的方法从头开始设计的。在所提出的框架的基础上，被称为ComScaN，是一个可扩展的，声明性的域特定语言（DSL）框架，使用一种新的演员模型。它设计有灵活和丰富的内置语言结构，以支持简化的规范和关注点分离。通过与灵活且可扩展的基于角色的DSL框架共同设计，项目团队正在为ComScaN开发一个正式的基础，其中包括一套语义模型，用于自动程序分析，验证和合成的正式方法和工具，目标是促进NFV缩放的定量性能推理。正在开发用于扩展NFV的定量性能推理技术以及用于验证服务功能链（SFC）的正确性和性能的算法，以及用于生成用于测试和评估SFC的动态工作负载的基于合成的方法。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

In today’s interconnected world, network operators need the ability to rapidly deploy, update, and scale services on-demand. Building such systems is challenging, and assuring their correctness and performance has been elusive. The project team aims to develop a “green field” approach to support future networks and emerging services in such a manner that scalability is inherent by design and correctness and performance claims can be backed up with mathematical rigor. This is achieved by bringing together and extending recent research advances in the areas of networking systems, programming languages, and software-verification methods. This is intended to provide network operators with the ability to express desired requirements for a diverse range of services, the flexibility to easily adapt those services to keep pace with changing demand and evolving network infrastructure, and the assurance that performance and correctness goals are upheld. The research is expected to produce a viable prototype demonstrating the core ideas along with an ecosystem of open-source software tools, experimental data and, example applications. The learnings from this project will be incorporated into the academic curriculum to equip the workforce with the skills needed to build reliable and performant networking infrastructure. The work is being carried out by attracting, engaging and mentoring a diverse group of budding researchers, with an intentional focus on welcoming and encouraging participation by hitherto under-represented groups in advanced computing research.In this project the principal investigators advance a green-field approach to enable quantitative performance reasoning of Network Function Virtualization (NFV) scaling. It is designed from the ground up based on formal foundations and principled approaches. At the basis of the proposed framework, referred to as ComScaN, is an extensible, declarative domain-specific language (DSL) framework using a novel actor model. It is designed with flexible and rich built-in language constructs to support ease of specification and separation of concerns. Co-designing with the flexible and extensible actor-based DSL framework, the project team is developing a formal foundation for ComScaN with a suite of semantic models, formal methods and tools for automatic program analysis, verification and synthesis, with the goal to facilitate quantitative performance reasoning of NFV scaling. Quantitative performance reasoning techniques for scaling NFV as well as algorithms for verifying correctness and performance of service function chains (SFCs) and synthesis-based approaches for generating dynamic workloads for testing and evaluation of SFCs are being developed.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.