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

运行时验证（RV）可以帮助在软件部署之前及早发现bug。RV根据正式的行为规范监视程序的执行，如果这些执行不满足规范，就会产生违规。之前的RV研究发现，在几十个开源项目中存在数百个bug。但是先前的研究使用的工具只针对Java编程语言，并检查用领域特定语言编写的规范，这对新的RV用户来说很难学习。这个项目的影响是通过创建支持其他编程语言和更简单规范格式的RV工具，使RV在开发人员中更广泛地用于bug查找。该项目的新颖之处在于，它针对常用的语言和格式，从而降低了新接触RV的开发人员进入的语言障碍，并使他们更容易编写规范。调查人员将培训本科生参与OpenMOP的开发，在他们的软件工程课程中创建OpenMOP模块，并在部署OpenMOP时评估其使用情况，以发现软件开发过程中的错误。这个项目提出OpenMOP来解决目前难以使用RV查找bug的基础设施缺陷。OpenMOP是一个RV基础设施，它构建并重用JavaMOP的部分内容——JavaMOP是Java的RV工具，自2002年以来一直在开发中。OpenMOP提供了两个新特性。首先，它使开发人员能够以他们已经熟悉的格式描述程序事件和属性。例如，在一种建议的格式中，开发人员可以定义在一小部分程序位置指定程序行为所需的程序事件，类似于为调试添加断点。其次，OpenMOP采用了与语言无关的客户机-服务器架构，可以针对不同的编程语言快速创建高效的RV工具。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.