Monitor-DPN 的可迭代前向可达性分析
计算机科学中的逻辑
2013-09-23 v1 分布式、并行与集群计算
编程语言
摘要
正如 Steffen 和 Schmidt 在九十年代所观察和研究的那样，数据流分析与模型检测之间存在密切联系。这表明，在无限状态模型检测领域开发的基于自动机的分析技术，可作为解释复杂控制结构的数据流分析器应用，从而推动了针对日益复杂模型的分析技术的发展。Esparza 和 Knoop 提出的一种方法基于计算自动机配置集的前驱集或后继集。我们的目标是调整并利用这种方法来分析多线程 Java 程序。具体而言，我们考虑用于并发程序的 Monitor-DPN 模型。Monitor-DPN 能够精确建模无界递归、动态线程创建以及通过良嵌套锁进行的同步，并对过程局部和线程局部状态进行有限抽象。此前关于该模型的工作展示了如何计算正则配置的正则前驱集以及固定初始配置的树正则后继集。通过结合和扩展先前开发的不同技术，我们展示了如何计算树正则集的树正则后继集。由此，我们获得了一种可迭代的、锁敏感的前向可达性分析。我们为该分析实现了针对 Java 程序的工具，并将其应用于信息流控制和数据竞争检测。
引用
@article{arxiv.1309.5150,
title = {Iterable Forward Reachability Analysis of Monitor-DPNs},
author = {Benedikt Nordhoff and Markus Müller-Olm and Peter Lammich},
journal= {arXiv preprint arXiv:1309.5150},
year = {2013}
}
备注
In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557