FMitF: Track I: Synthesizing Semantic Checkers for Runtime Verification of Production Distributed Systems

随着用户越来越依赖分布式系统来提供各种服务，确保这些系统正常运行至关重要。然而，软件错误和硬件故障可能会导致生产分布式系统违反语义保证，而不会显示任何显式错误。这些“无声故障”可能会产生严重的后果，并且难以使用现有方法检测。解决这个问题的一个很有前途的方法是使用可以检测语义违规的运行时检查器来持续验证系统行为。不幸的是，很少有生产分布式系统采用了运行时验证，由于相关的困难和成本，创建强大而有效的检查。该项目旨在通过设计新的端到端方法来弥合这一根本性差距，这些方法可以自动合成现代分布式系统的高质量语义检查器。该项目将产生一个框架，该框架利用开发人员已经为特定系统输入编写的许多现有测试，通过分析测试代码并生成在新输入下正确执行的语义检查器。该项目将进一步建立一种新的语言和相应的运行时验证器，以生成更具表现力和效率的检查器，并随着系统的发展而改进检查器。无声的故障导致了重大损失和中断。该项目将使大规模分布式系统对无声的语义故障具有弹性，并减少其对用户和社会的影响。此外，它将提高对分布式系统运行时验证的认识和理解，并提供实用的工具链，促进其广泛采用。该项目包括教育和外展活动，包括学生辅导，课程开发，软件（及相关）工件的发布，以及通过各种学术和行业场所传播结果。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

As users increasingly depend on distributed systems to provide various services, it is critical to ensure that these systems function properly. However, software bugs and hardware faults can cause production distributed systems to violate semantic guarantees without demonstrating any explicit errors. These "silent failures" can have serious consequences and are difficult to detect using existing methods. One promising approach to this problem involves continuous verification of system behavior using runtime checkers that can detect semantic violations. Unfortunately, few production distributed systems have adopted runtime verification due to the associated difficulty and cost of creating robust and efficient checkers. This project aims to bridge this fundamental gap by designing new, end-to-end methods that automatically synthesize high-quality semantic checkers for modern distributed systems. The project will result in a framework that leverages the many existing tests developers have already written for particular system inputs by analyzing the test code and generating semantic checkers that perform correctly under new inputs. The project will further establish a new language and corresponding runtime verifier to generate more expressive and efficient checkers and to refine the checkers as the system evolves.Distributed systems are the backbone of vital services in our society. Silent failures have led to significant losses and disruptions. This project will make large-scale distributed systems resilient to silent semantic failures and reduce their impact on users and society. Furthermore, it will increase awareness and understanding of runtime verification for distributed systems and provide practical toolchains that facilitate its widespread adoption. The project includes education and outreach activities that include student mentoring, curriculum development, release of software (and related) artifacts, and dissemination of results through a variety of academic and industry venues.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.