乱序数据流上时序属性的运行时验证
计算机科学中的逻辑
2017-07-19 v1
摘要
我们提出一种在运行时验证系统的监控方法。我们的方法面向那些组件通过不可靠信道与监控器通信的系统，其中消息可能被延迟或丢失。与先前工作将属性规约语言局限于命题时序逻辑不同，我们的方法处理了带冻结量词（用于推理数据值）的实时逻辑 MTL 的扩展。我们给出了其基于一种新的三值语义的基础理论，该语义非常适合在消息延迟或丢失存在的情况下对事件流进行可靠且完备的在线推理。我们还通过实验评估了该方法。我们的原型实现在消息乱序接收的设置下每秒处理数百个事件。
引用
@article{arxiv.1707.05555,
title = {Runtime Verification of Temporal Properties over Out-of-order Data Streams},
author = {David Basin and Felix Klaedtke and Eugen Zălinescu},
journal= {arXiv preprint arXiv:1707.05555},
year = {2017}
}
备注
long version of the CAV 2017 paper