论文标题
有限状态属性对有损事件流的最佳运行时验证
Optimal Runtime Verification of Finite State Properties over Lossy Event Streams
论文作者
论文摘要
由于高内存和执行时间开销，监视有限状态属性的程序具有挑战性。某些事件如果自然跳过或失去可以减少两个开销，但会导致当前监视器状态的不确定性。在这项工作中，我们提出了一个理论框架，以对这些有损事件流进行建模，并为监视器提供一个构造，该监视器观察它们而不会产生假阳性。在所有完整的监视器中，构造的显示器在最佳状态下是最佳的。我们使用我们的框架对几种实际相关性进行建模，并为具有大量状态的属性构建较小的近似显示器。
Monitoring programs for finite state properties is challenging due to high memory and execution time overheads it incurs. Some events if skipped or lost naturally can reduce both overheads, but lead to uncertainty about the current monitor state. In this work, we present a theoretical framework to model these lossy event streams and provide a construction for a monitor which observes them without producing false positives. The constructed monitor is optimally sound among all complete monitors. We model several loss types of practical relevance using our framework and provide construction of smaller approximate monitors for properties with a large number of states.
