LTL 性质无状态模型检测的新方法
编程语言
2016-03-14 v1
摘要
大型复杂并发程序的验证是软件领域的一个重要问题。无状态模型检测是一种对大型程序进行系统和自动测试的合适方法，其在验证大型程序代码方面已证明功效。该领域中另一种著名的方法是运行时验证。无状态模型检测与运行时验证在某些方面相似。运行时验证中的一种常见方法是为用线性时序逻辑表达的性质构造运行时监视器。当前，运行时验证领域提出了一些在有限路径上检查线性时序逻辑公式的语义，其也可应用于无状态模型检测。然而，现有的无状态模型检测器不支持 LTL 公式。在某些设置下，利用无状态模型检测而非运行时验证更具优势。本文提出了一种将近期有限路径上 LTL 语义之一编码进基于 actor 的系统中的新方案。我们采取真正并行的方法，不保存任何程序状态或轨迹，这不仅解决了运行时验证中的重要问题，也可应用于无状态模型检测。
引用
@article{arxiv.1603.03535,
title = {A New Approach to Stateless Model Checking of LTL Properties},
author = {Elaheh Ghassabani and Mohammad Abdollahi Azgomi},
journal= {arXiv preprint arXiv:1603.03535},
year = {2016}
}