As computing innovation continues to accelerate in our technology-driven world, some of the latest software advancements are outpacing their systems, creating additional challenges for engineers. Rather than pulling the plug on existing tools, Rahul Purandare proposes plugging in a new solution.
With support from the National Science Foundation and its Formal Methods in the Field (FMitF) initiative, Purandare, an associate professor in the University of Nebraska–Lincoln’s School of Computing, will collaborate with Owolabi Legunsen, assistant professor at Cornell University, to streamline runtime verification of programs with new optimization tools and techniques compatible with both new and existing open-source frameworks.
Software runtime verification (RV) methods monitor program executions to ensure program correctness, detecting sometimes hundreds of bugs in open-source systems that were missed during the testing process. While RV is usually an effective and widely used solution for improving systems, it’s often an inefficient one, particularly for the implementation of faster tools. Optimizations to increase speed exist in literature, but there is no easy-to-use solution that implements them all in a pluggable fashion.
Purandare and Legunsen aim to change this with a new solution called OPTMOP, a sustainable framework that will make RV optimizations “pluggable” into existing implementations of inefficient monitoring algorithms and programming tools. OPTMOP will accelerate current RV methods during software testing and serve as a platform for designing and evaluating future RV optimizations.
“There is a surprising lack of open-source tools and frameworks that support the integration of optimizations in a modular, reusable way,” Purandare said. “OPTMOP addresses this gap by enabling developers to seamlessly integrate both established and novel RV optimizations into their existing development workflows.”
Purandare and Legunsen will develop OPTMOP by re-engineering two of their own monitoring-oriented programming tools: TraceMOP, an actively maintained and modernized fork of JavaMOP for Java, and PyMOP, a new tool in development for Python. Within those updated tools, they’ll re-implement three of their previously developed framework optimizations: stutter-equivalent loop transformation, which targets program loops generating large numbers of redundant events, residual analysis, which identifies program regions where events can be summarized or abstracted, and monitor compaction, which reduces runtime overhead by merging or restructuring multiple monitors.
Finally, the investigators will develop plugins that enable application of new or existing optimizations to their tools without modifying their core implementations. They’ll also evaluate their framework-enhanced tools by comparing them to other state-of-the-art tools and assessing how easily new optimizations can be plugged into the framework.
“To our knowledge, this will be the first open-source implementation of pluggable RV optimizations, along with a large-scale evaluation of their effectiveness across numerous open-source projects,” Purandare said.
According to Purandare, this work will produce an open-source framework that not only accelerates RV but also lowers the barrier for researchers and practitioners to plug additional optimizations directly into RV tools. He said it would also address a longstanding disconnect between those who design monitoring algorithms and those who optimize them.
“Developers currently have limited means to plug in new optimizations or take advantage of existing ones without significant manual effort or tool modification,” Purandare said. “With OPTMOP, programmers can focus on writing code and specification without needing to grapple with the complexities of verification internals. This streamlined process empowers developers to detect bugs earlier, reduce runtime overhead, and ultimately deliver more robust, higher-quality software.”
Purandare said this project could change the way developers use and even view RV techniques, paving the way for new software engineering breakthroughs that will work on a variety of systems in the future.
“The most exciting aspect of this project is its potential to reshape how developers interact with runtime verification, transforming it from a specialized, high-overhead technique into a practical, developer-friendly component of everyday software engineering.”
