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.