An On-The-Fly Algorithm for Conditional Weighted Pushdown Systems
An On-The-Fly Algorithm for Conditional Weighted Pushdown Systems
复制标题
DOI：
10.2197/ipsjtrans.7.132
复制
发表时间：
2014-08
期刊：
影响因子：
--
通讯作者：
Hua Vy Le Thanh;Xin Li
中科院分区：
文献类型：
--
作者：
Hua Vy Le Thanh;Xin Li
下推系统（PDS）是递归顺序程序的抽象模型，加权下推系统（WPDS）是程序分析中求解某些全路交会问题的一般框架。条件WPDS（CWPDS）进一步扩展了WPDS以增强WPDS的表达性，其中每个转换由堆栈上的正则语言保护，该堆栈指定可以应用转换规则的条件。CWPDSs或其实例在面向对象程序分析、访问权限分析等方面有着广泛的应用。模型检测CWPDSs被简化为模型检测WPDSs，并给出了一种离线算法，通过同步底层PDS和接受正则条件的有限状态自动机，将CWPDSs转换为WPDSs。然而，这种平移会导致系统的指数爆破。本文提出了一种CWPDS的动态模型检测算法，该算法在计算规则配置的后映像时按需调用计算机器。我们开发了一个动态的模型检查器CWPDS和应用它生成的模型从HTML5解析器规范的可达性分析。我们的初步实验表明，在飞行算法大大优于离线算法的实际空间和时间效率。
Pushdown systems (PDSs) are well-understood as abstract models of recursive sequential programs, and weighted pushdown systems (WPDSs) are a general framework for solving certain meet-over-all-path problems in program analysis. Conditional WPDSs (CWPDSs) further extend WPDSs to enhance the expressiveness of WPDSs, in which each transition is guarded by a regular language over the stack that specifies conditions under which a transition rule can be applied. CWPDSs or its instance are shown to have wide applications in analysis of objected-oriented programs, access rights analysis, etc. Model checking CWPDSs was shown to be reduced to model checking WPDSs, and an offline algorithm was given that translates CWPSs to WPDSs by synchronizing the underlying PDS and finite state automata accepting regular conditions. The translation, however, can cause an exponential blow-up of the system. This paper presents an on-the-fly model checking algorithm for CWPDSs that synchronizes the computing machineries on-demand while computing post-images of regular configurations. We developed an on-the-fly model checker for CWPDSs and apply it to models generated from the reachability analysis of the HTML5 parser specification. Our preliminary experiments show that, the on-the-fly algorithm drastically outperforms the offline algorithm regarding both practical space and time efficiency.