CAREER: Specializing Runtime Verification for Software Testing

Software testing is usually the last line of defense against bugs. But testing misses bugs, so costly and harmful bugs often occur in deployed software. Techniques that can help find more bugs during testing are needed.

Runtime verification is one such technique; it finds bugs by checking program runs against formal specifications that describe correct program behavior. This project seeks to make runtime verification more effective and more efficient. The project also aims to facilitate teaching runtime verification to software engineers by creating a course on runtime verification, integrating runtime-verification modules into a software-testing course, and creating publicly available pedagogical materials and open-source tools.

The project focuses on addressing four major impediments to runtime-verification usage: (1) most signaled violations are false alarms, because existing specifications are inadequate; (2) confirming whether a signaled violation is a bug takes too much developer time; (3) runtime verification does not scale to the large software systems on which society increasingly depends; and (4) it is expensive for developers to write tests that cover code where specifications may be violated. Automated solutions to address these impediments will require fundamental advances in operations on traces -- sequences of program events -- that are generated during runtime verification.

Consequently, this project will develop a trace-aware runtime-verification technique that works directly on traces. Automated techniques based on trace-aware runtime verification will also be developed to (1) reduce false alarms by repairing existing specifications; (2) classify each violation as a likely bug or false alarm; (3) reduce redundant computations performed during runtime verification; and (4) generate tests automatically to adequately check code with respect to the specifications.

The project's main impact is to bring runtime verification closer to helping developers find more bugs during every test run.

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.