具有程序的静态结构和动态行为语义的时序逻辑

摘要

提出一种区间分支时序逻辑———控制流区间时序逻辑（control flow interval temporal logic ， CFITL），用于规约程序的时序属性。不同于计算树逻辑（computation tree logic ，CTL）和线性时序逻辑（linear temporal logic ，LTL）等传统的时序逻辑，CFITL 公式的语义模型不是基于状态的类 Kripke 结构，而是以程序的抽象模型控制流图（control flow graph ，CFG）为基础所构建的含序 CFG 结构。含序CFG 是 CFG 的一种受限子集，它们的拓扑结构可映射为偏序集，这样诱导产生的自然数区间可自然地用于描述定义良好的程序结构。这种结构含有程序的静态结构信息和动态行为信息，换而言之，CFITL具有规约程序实现结构属性和程序执行动态行为属性的能力。在定义 CFITL 的语法和语义的基础上，详细讨论了 CFITL 的模型检验问题，包括基于值状态空间可达性计算的模型检验方法和基于 SM T （satisfiability modulo theories）的 CFITL 有界模型检验方法。现代程序都含有复杂且具有无限值域的抽象数据类型及各种复杂的操作，CFITL 语义定义相比 CTL 等时序逻辑更复杂，因此，基于显示状态搜索的方法难以有效进行，而基于 SM T 的 CFITL 有界模型检验方法更易实现、更具有可行性。最近开发相关的原型工具，并进行相关的实例研究。%The paper presents an interval temporal logic — CFITL(control flow interval temporal logic) which is used to specify the temporal properties of abstract model of program ,for example control flow graph , generally abbreviated to CFG . The targeted logic differs from the general sense of temporal logics ,typically CTL and LTL ,whose semantical models are defined in term of the state‐based structures .The semantics of CFITL is defined on an ordered CFG structure ,which encodes the static structure and dynamic behavior of program .The ordered CFGs are a subset of CFGs ,and their topology can be summarized by partially ordered sets ,such that the induced natural number intervals can be mapped onto the well‐formed structures of program .In other words ,the CFITL formulae have the ability of specifying the properties related to not only the dynamic behavior but also static structure of programs . After the syntax and semantics of CFITL are expounded , the problem of model checking over CFITL is detailedly discussed . Furthermore , two types of algorithms are designed :one is based on the computation of reachable state space as well as the another is based on bounded model checking employing the SM T (satisfiability modulo theories) solvers power .Because programs implemented by advanced programming languages inevitably involve complex abstract data types with unbounded domains and operators ,and the semantics of CFITL is more complex than the one of CTL ,the method of SM T based model checking is more practical than the method of direct search of state space .In the sequel ,a prototype tool is implemented ,and some case studies are conducted .