一句话：提出 Valg——首个用强化学习实现选择性在线运行时验证的技术，以两臂老虎机剪枝冗余监视器，最高加速 551.5 倍。
运行时验证（RV）用形式规约动态合成的监视器检查运行中的程序，能在开源项目测试中发现大量缺陷，但高开销使其难以实用。作者发现 99.87% 的监视器在测试中是冗余的，它们重复检查其他必要监视器已覆盖过的唯一 trace（事件序列）。据此提出 Valg：首个面向测试的在线选择性 RV 技术，也是首个用强化学习加速 RV 的工作。它根据既往监视器与事件的冗余反馈，仅监控后续必要的监视器；关键创新是把选择性监视器创建形式化为两臂老虎机问题，奖励必要监视器、惩罚冗余监视器。其 Java 实现比 JavaMOP 快至多 20.2 倍、比 TraceMOP 快 551.5 倍，仍检出二者 99.6% 的规约违反，平均只检查 76.7% 的唯一 trace；调参后可检查 95.1% 的唯一 trace，且超参跨 revision 复用仍保持加速。
Runtime verification (RV) uses monitors, which are dynamically synthesized from formal specifications (specs), to check running programs against specs. RV of passing tests in many open-source projects found hundreds of new bugs. But, high overheads make it hard to use RV for testing in practice.We propose Valg, the first on-the-fly selective RV technique for testing, and the first to use reinforcement learning (RL) to speed up RV. Valg leverages a recent finding: 99.87% of monitors are redundant for testing; they wastefully re-check unique traces— sequences of events, e.g., method calls—that the other necessary 0.13% already checked. Valg uses feedback about redundancy of prior monitors and events to selectively monitor only necessary ones subsequently. A key idea in Valg is our novel formulation of selective monitor creation as a two-armed bandit RL problem that rewards necessary monitors and penalizes redundant ones.We implement Valg for Java and compare it with state-of-the-art RV tools on one revision each of 64 open-source projects. With default RL hyperparameters, Valg is up to 20.2x and 551.5x faster than JavaMOP and TraceMOP, respectively. For example, Valg takes only 11.6 minutes in total to monitor three projects where TraceMOP takes 3.02 days in total. With default RL hyperparameters, Valg finds 99.6% of spec violations found by JavaMOP and TraceMOP, but it only checks 76.7% of their unique traces on average. After tuning RL hyperparameters, Valg checks 95.1% of unique traces on average with minor loss in speed. Using tuned hyperparameters from one revision "into the future" as code evolves preserves Valg’s high speedups and rate of checked unique traces, without needing frequent re-tuning.
DOI 原文 ·
@inproceedings{paperbot9440,
title = {Faster Runtime Verification during Testing via Feedback-Guided Selective Monitoring},
author = {Shinhae Kim and Saikat Dutta and Owolabi Legunsen},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00189}
}