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

一般来说，网络系统，尤其是互联网，是涉及许多相互作用的组件的复杂系统。在众多网络协议中实现的网络控制算法是这些系统的核心。到目前为止，网络控制算法的设计和分析一直是基于启发式的和理想化的网络模型，在实践中对其性能没有任何保证。该方案旨在解决这一缺陷，并发展各种方法来证明网络控制算法的性能，并综合具有性能证明的算法。网络控制算法的创新正在以快速的速度发生，原因是不断发展的网络技术、快速变化的应用组合以及对用户体验质量日益重要的影响，用户对糟糕的性能做出负面反应(例如，通过给予应用程序较差的评级或寻找替代方案)。业绩不仅关系到平均值，也关系到尾部统计数据。对此，研究界和业界开发了许多创新的网络控制算法来提高性能。尽管取得了这些进展，但人们对这些算法的性能保证知之甚少，也没有一个原则性的证明驱动的框架来帮助这些算法的开发。本文提出的研究如果成功，将提高社区验证性能属性和合成具有可证明属性的新算法的能力。所提出的工具将为网络资源分配研究开辟新的方向。该教育计划包括将这项研究的结果纳入本科生和研究生课程，并为学生提供使用VERITAS的工具实施可验证的网络控制算法的机会，将性能视为正确性。该建议开发了一个框架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.