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

Cornell University, Ithaca NY

Investigators

Abstract

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.