Collaborative Research: CNS Core: Medium: Robust Behavioral Analysis and Synthesis of Network Control Protocols Using Formal Verification

网络系统，特别是互联网，是一个复杂的系统，涉及许多相互作用的组件。在许多网络协议中实现的网络控制算法是这些系统的核心。到目前为止，网络控制算法的设计和分析一直是基于数学和理想化的网络模型，没有任何保证其性能在实践中。该建议旨在解决这一缺点，并开发方法来证明网络控制算法的性能特性，并综合算法与性能证明。网络控制算法的创新正在以快速的速度发生，这是由不断发展的网络技术、快速变化的应用组合以及用户体验质量的日益重要性所推动的，用户对较差的性能（例如，通过给予应用程序差的评级或寻找替代方案）。业绩不仅在均值方面很重要，在尾部统计数据方面也很重要。作为回应，研究界和工业界已经开发了许多创新的网络控制算法来提高性能。尽管有这些进步，很少有人知道这些算法的性能保证，也没有原则性的证明驱动的框架，以帮助这些算法的发展。本文提出的研究，如果成功的话，提高社区的能力，以验证性能属性和合成新的算法与可证明的属性。在拟议的工作中产生的工具将打开网络资源分配研究的新方向。该教育计划包括将这项研究的结果纳入本科和研究生课程，并为学生提供一个机会，实现可验证的网络控制算法使用的工具从Veritas，治疗性能的corrects.This建议开发一个框架，Veritas，它使用形式验证来证明性能属性的网络控制算法。使用Veritas，用户可以（1）以一阶逻辑编码算法，（2）指定关于算法的假设，以及（3）通过在可定制的内置环境模型中运行编码算法来测试假设是否成立。此外，给定控制算法的约束条件--算法可用的输入观测值和它可以响应观测值的动作空间--沿着以一阶逻辑编码的环境模型和性能目标的规范，Veritas自动搜索控制器的空间，以提出输入观测和控制器动作之间的映射。该奖项反映了NSF的法定使命，通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Networked systems in general, and the Internet in particular, are complex systems involving many interacting components. Network control algorithms implemented in numerous network protocols are at the core of these systems. To date, the design and analysis of network control algorithms has been based on heuristics and idealized models of networks, without any guarantees on their performance in practice. This proposal aims to address this shortcoming and develop methods to prove performance properties of network control algorithms and to synthesize algorithms with performance proofs. Innovations in network control algorithms are occurring at a rapid pace, spurred by evolving network technologies, a fast-changing application mix, and the rising importance of quality-of-experience for users, who react negatively to poor performance (e.g., by giving applications poor ratings or finding alternatives). Performance matters not only in the mean, but also in the tail statistics. In response, the research community and industry have developed numerous innovative network control algorithms to improve performance. Despite these advances, little is known about performance guarantees of such algorithms, nor is there is principled proof-driven framework to help the development of these algorithms. The research proposed herein will, if successful, improve the community's ability to verify performance properties and synthesize new algorithms with provable properties. The tools produced in the proposed work will open new directions in network resource allocation research. The education plan includes the incorporation of this research's findings into the undergraduate and graduate curricula and offers students an opportunity to implement verifiable network control algorithms using the tools from Veritas, treating performance as correctness.This proposal develops a framework, Veritas, which uses formal verification to prove performance properties of a network control algorithm. With Veritas a user can (1) encode an algorithm in first-order logic, (2) specify a hypothesis about the algorithm, and (3) test if the hypothesis holds by running the encoded algorithm in a customizable, built-in environment model. In addition, given constraints on a control algorithm---input observations usable by the algorithm and an action space over which it can respond to observations---along with the environment model encoded in first-order logic and a specification of performance objectives, Veritas automatically searches over the space of controllers to propose a mapping between input observations and controller actions.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.