FMitF: Track II: eMOP: A Tool for Evolution-Aware Runtime Verification

Cornell University, Ithaca NY

Investigators

Abstract

Most software developers perform regression testing, re-running tests after every code change, to check that new bugs are not being introduced. Unfortunately, regression testing often misses bugs. This project is developing eMOP, a runtime-verification tool for discovering more bugs during regression testing. Runtime verification checks test runs against specifications that are encoded as logical formulas. Test runs that do not satisfy the specifications result in violations. This project has three infrastructure thrusts. First, a core eMOP component is created that incrementally applies runtime verification, for example, by rechecking only specifications that can be violated in parts of code affected by the changes. Second, the core component is integrated with popular open-source regression testing infrastructure: build systems, continuous integration, and integrated development environments. Third, the core component is enhanced with features for prioritization and improved reporting that make it easier to triage, inspect, and debug violations. When complete, eMOP will offer the bug-finding benefits of runtime verification within regression testing infrastructure that developers already use. The project brings the results of decades of runtime verification research to a wider audience of software developers. eMOP enables developers to find more bugs earlier -- ideally as soon as the bugs are introduced. By using eMOP, students will also be introduced to lightweight formal methods within a software-engineering curriculum. Graduate and undergraduate students, including underrepresented minorities, will be involved, and they will gain exposure to software engineering and lightweight formal methods. The eMOP code will be released publicly on GitHub (https://github.com/SoftEngResearch/emop) under the Apache License 2.0. The code will be maintained for a minimum of three years. A supplementary web page linked from the GitHub repository will contain tutorials and experimental data. 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.