LTL Model Checking for Register Pushdown Systems
LTL Model Checking for Register Pushdown Systems
复制标题
DOI：
10.1587/transinf.2020edp7265
复制
发表时间：
2021-12
期刊：
影响因子：
--
通讯作者：
Ryoma Senda;Y. Takata;H. Seki
中科院分区：
文献类型：
--
作者：
Ryoma Senda;Y. Takata;H. Seki
下推系统（PDS）是递归程序的抽象模型。对于PDS，模型检查方法已被研究并应用于各种软件验证，例如过程间数据流分析和恶意软件检测。但是，PDS不能操作来自无限域的数据值。寄存器PDS（RPDS）是PDS的扩展，通过添加寄存器以受限方式处理数据值。本文提出了RPDS的LTL模型检测问题的算法，具有简单和规则的赋值，这是原子命题的配置与合理的限制的标签。首先，我们介绍了RPDS和相关模型，然后定义了RPDS的LTL模型检测问题。其次，我们给出了解决这些问题的算法，并证明了这些问题是EXPTIME完全的。作为实际的例子，我们展示了解决方案的恶意软件检测和XML模式检查所提出的框架。
SUMMARY A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.