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

FMITF：第一轨：综合语义检查器以进行生产分布式系统的运行时验证

• 批准号: 2318937
• 负责人: Peng Huang
• 金额: $ 75万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318937&HistoricalAwards=false
• 关键词: FMitF; Track; Synthesizing; Semantic; Checkers

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.

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