面向含部分信息的时序事件流的运行时验证
计算机科学中的逻辑
2019-07-19 v1 形式语言与自动机理论
编程语言
摘要
运行时验证（Runtime Verification, RV）研究如何分析被观测系统的执行迹。流运行时验证（Stream Runtime Verification, SRV）应用流变换从观测迹中获取信息。信息缺失于间隙的不完整迹在将 RV 与 SRV 技术应用于真实系统时构成常见挑战，因为 RV 方法通常需要无缺失部分的完整迹。本文提出一种基于抽象在不完整迹上执行 SRV 的方案。我们使用 TeSSLa 作为非同步时序事件流的规约语言，并定义抽象事件流以表示输入迹间隙期间可能发生过的所有迹的集合。我们展示如何将 TeSSLa 规约翻译为其抽象对应体，该对应体可在输入流的变换中传播间隙，从而即便输入流含有间隙与取值不精确的事件也能生成可靠输出。该方案已作为原 TeSSLa 的一组宏实现，实证评估显示了该方法的可行性。
引用
@article{arxiv.1907.07761,
title = {Runtime Verification For Timed Event Streams With Partial Information},
author = {Martin Leucker and César Sánchez and Torben Scheffel and Malte Schmitz and Daniel Thoma},
journal= {arXiv preprint arXiv:1907.07761},
year = {2019}
}