高级检索
    陈冬火, 刘全, 金海东, 朱斐, 王辉. 具有程序的静态结构和动态行为语义的时序逻辑[J]. 计算机研究与发展, 2016, 53(9): 2067-2084. DOI: 10.7544/issn1000-1239.2016.20150370
    引用本文: 陈冬火, 刘全, 金海东, 朱斐, 王辉. 具有程序的静态结构和动态行为语义的时序逻辑[J]. 计算机研究与发展, 2016, 53(9): 2067-2084. DOI: 10.7544/issn1000-1239.2016.20150370
    Chen Donghuo, Liu Quan, Jin Haidong, Zhu Fei, Wang Hui. A Temporal Logic with a Semantics Defined on the Static Structure and Dynamic Behavior of Program[J]. Journal of Computer Research and Development, 2016, 53(9): 2067-2084. DOI: 10.7544/issn1000-1239.2016.20150370
    Citation: Chen Donghuo, Liu Quan, Jin Haidong, Zhu Fei, Wang Hui. A Temporal Logic with a Semantics Defined on the Static Structure and Dynamic Behavior of Program[J]. Journal of Computer Research and Development, 2016, 53(9): 2067-2084. DOI: 10.7544/issn1000-1239.2016.20150370

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

    A Temporal Logic with a Semantics Defined on the Static Structure and Dynamic Behavior of Program

    • 摘要: 提出一种区间分支时序逻辑——控制流区间时序逻辑(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的模型检验问题,包括基于值状态空间可达性计算的模型检验方法和基于SMT(satisfiability modulo theories)的CFITL有界模型检验方法. 现代程序都含有复杂且具有无限值域的抽象数据类型及各种复杂的操作,CFITL语义定义相比CTL等时序逻辑更复杂,因此,基于显示状态搜索的方法难以有效进行,而基于SMT的CFITL有界模型检验方法更易实现、更具有可行性.最近开发相关的原型工具,并进行相关的实例研究.

       

      Abstract: 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 SMT(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 SMT 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.

       

    /

    返回文章
    返回