Collaborative Research: FMitF: Track II: Cross-Language Support for Runtime Verification

合作研究：FMitF：轨道 II：运行时验证的跨语言支持

• 批准号: 2319473
• 负责人: Owolabi Legunsen
• 金额: $ 5万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-09-01 至 2025-02-28
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319473&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; II

Runtime verification (RV) can help find bugs early, before the software is deployed. RV monitors program executions against formal behavioral specifications and generates violations if those executions do not satisfy the specifications. Prior RV research found hundreds of bugs in scores of open-source projects. But that prior research used tooling that only targets the Java programming language and checks specifications written in a domain-specific language that is hard for new RV users to learn. This project’s impact is to make RV more widely used for bug finding among developers by creating RV tool support for other programming languages and simpler specification formats. The project’s novelty is that it targets commonly-used languages and formats to lower the language barriers to entry for developers who are new to RV, and makes it easier for them to write specifications. The investigators will train undergraduate students to participate in developing OpenMOP, create modules on OpenMOP in their software engineering classes, and evaluate OpenMOP usage when deploying it to find bugs during software development.This project proposes OpenMOP to address infrastructure gaps that today make it hard to use RV to find bugs. OpenMOP is an RV infrastructure that builds on and reuses parts of JavaMOP -- an RV tool for Java that has been in development since 2002. OpenMOP provides two new features. First, it enables developers to describe program events and properties in formats that they are already familiar with. For example, in one proposed format, developers can define the program events needed to specify program behavior at a small set of program locations, similar to adding breakpoints for debugging. Second, OpenMOP adopts a language-agnostic client-server architecture to enable the rapid creation of efficient RV tools for different programming languages.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.

在部署软件之前，运行时验证（RV）可以帮助早日查找错误。 RV监视计划对正式行为规格的执行，如果执行不符合规格，则会造成违规行为。先前的RV研究发现数百个开源项目中的错误。但是，这项先前的研究使用了仅针对Java编程语言的工具，并检查了用特定于领域的语言编写的规范，这对于新的RV用户来说很难学习。该项目的影响是通过为其他编程语言和更简单的规范格式创建RV工具支持，使RV在开发人员之间更广泛地使用。该项目的新颖性是，它针对常用的语言和格式，以降低RV新手的开发人员的语言障碍，并使他们更容易编写规格。调查人员将培训本科生参与开发OpenMop，在其软件工程课程中在OpenMop上创建模块，并在部署其在软件开发过程中查找错误时评估OpenMOP使用情况。该项目提案OpenMOP解决了基础架构差距，以解决今天很难使用RV的基础架构差距。 OpenMop是一款RV基础架构，基于Javamop的一部分，这是Java的一部分，这是Java的RV工具，自2002年以来一直在开发中。OpenMop提供了两个新功能。首先，它使开发人员能够以他们已经熟悉的格式描述程序事件和属性。例如，以一种建议的格式，开发人员可以定义在一小部分程序位置指定程序行为所需的程序事件，类似于添加用于调试的断点。其次，OpenMOP采用语言不可或缺的客户服务器体系结构，以快速为不同的编程语言创建有效的RV工具。该奖项反映了NSF的法定任务，并通过使用基金会的知识分子优点和更广泛的影响标准来评估NSF的法定任务。