FMitF: Track I: Performance Verification for Networked Systems

The networked services that our modern society depends on require many types of resources, including computing power, memory and energy from the end user’s device, network resources from the cellular network provider and massive storage and computation facilities in warehouse-sized data centers. These systems rely on many complex algorithms that decide when to allocate which resources to which users and applications. A key unmet challenge in designing these algorithms is evaluation. How can an engineer be certain that their design will make good decisions in the increasingly complicated infrastructure that operates modern networked applications? Testing helps but does not account for phenomena that may be encountered during deployment but were not a part of the tests. This project develops performance verification, a suite of automated reasoning tools that can search vast spaces of possible system behaviors to find any that result in degraded performance. By providing more principled and more automated methods of evaluation, the project enables system engineers to design more reliable and available systems. This, in turn, provides benefits for a wide range of critical services that depend on the reliable performance of networked infrastructure, including utilities, aviation, defense and first responders. The techniques developed in this project are incorporated into university courses and publicly disseminated educational materials. Performance verification entails assumption-constrained worst-case analysis, which makes it easier to model the complex behavior of real-world systems and does not require the precise characterization of the system and workload required by traditional methods (e.g., simulation). Today, performance verification is a nascent field. To create impact at scale, it needs formalization, better automated reasoning methods, and more systematic ways to connect formal models to the underlying implementations. This project develops a formal modeling and specification framework to model networked systems and specify performance properties. Based on a hybrid of network calculus and discrete control, it provides a practical trade-off between expressiveness and amenability to formal reasoning. In contrast to existing approaches, the framework allows the modeling of closed-loop control while achieving a high degree of automation. The project explores techniques to automatically generate proofs and counterexamples, applying methods such as syntax-guided synthesis, counterexample-guided inductive synthesis, and Satisfiability Modulo Theories (SMT) solving. Finally, to bridge the gap between the formally verified model and the actual system implementation, the framework provides support for validating these formal models against actual implementations or real-world network data. 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.