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的法定任务，并被认为值得通过基金会的知识分子和更广泛的影响来通过评估来获得支持。