使用单子差分逻辑的时序运行时验证
计算机科学中的逻辑
2007-06-01 v1
摘要
在本文中，我们提出了一种在定时运行上对有界时序逻辑执行运行时验证的算法。该算法由三个要素组成。首先，将待验证的有界时序公式翻译为差分不等式上的单子一阶逻辑，我们称之为单子差分逻辑。其次，在定时运行的每一步，通过计算该步的状态和时间与单子差分公式的商来修改该公式。第三，通过单子差分逻辑的判定过程，检查所得公式是否为重言式或不可满足的。我们进一步提供了一种基于差分决策图数据结构的简单单子差分逻辑判定过程。对于被刻画为齐次单子的时序公式子类，该算法在非常强的意义上是完备的，而在其他公式上则是近似的。这种近似源于并非所有不可满足或重言式的公式都能在运行时验证的最早可能时间被识别。与现有方法相反，本文提出的算法不通过语法重写工作，而是采用高效的决策结构，使其适用于例如商业软件等实际应用中。
引用
@article{arxiv.0705.4604,
title = {Temporal Runtime Verification using Monadic Difference Logic},
author = {Henrik Reif Andersen and Kaare J. Kristoffersen},
journal= {arXiv preprint arXiv:0705.4604},
year = {2007}
}