关于参数化轨迹切片、垃圾回收与静态分析的故事

本文提出了一种设想（故事），探讨如何通过静态检测不可达对象（在 Java 中）来改进一种特定的运行时验证方法（针对 Java），即参数化轨迹切片。用于参数化轨迹切片的监控算法依赖垃圾回收来 (i) 清理存储被监控对象的数据结构，确保其不会变得过大而难以管理，以及 (ii) 预测非安全性属性的违反，因为当被监控对象后续无法再出现在轨迹中时，这些属性便无法被满足。本文的设想是，通过在参数化属性中明确被监控对象的不可达性，并静态地引入生成相关事件的额外插桩点，可以改进这两种用途。本文提出的想法仍处于探索阶段，其目标是将所描述的技术集成到用于量化事件自动机的 MarQ 监控工具中。