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

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

作　　者：陈冬火[1] 刘全[1,2] 金海东[1] 朱斐[1,2] 王辉[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]符号计算与知识工程教育部重点实验室(吉林大学),长春130012

出　　处：《计算机研究与发展》2016年第9期2067-2084,共18页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61272005;61303108;61373094;61472262;61502323;61502329);江苏省自然科学基金项目(BK2012616);福建省自然科学基金项目(2014J01221);江苏省高校自然科学研究项目(13KJB520020);吉林大学符号计算与知识工程教育部重点实验室项目(93K172014K04);苏州市应用基础研究计划项目(SYG201422)~~

摘　　要：提出一种区间分支时序逻辑——控制流区间时序逻辑(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有界模型检验方法更易实现、更具有可行性.最近开发相关的原型工具,并进行相关的实例研究.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.

关 键 词：区间时序逻辑 控制流程图 程序静态结构 模型检验 可满足性模理论 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]