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

来源：计算机研究与发展杂志2016年第9期北京时间：

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

摘要：提出一种区间分支时序逻辑——控制流区间时序逻辑(controlflowintervaltemporallogic,CFITL)，用于规约程序的时序属性.不同于计算树逻辑(computationtreelogic,CTL)和线性时序逻辑(lineartemporallogic,LTL)等传统的时序逻辑，CFITL公式的语义模型不是基于状态的类Kripke结构，而是以程序的抽象模型控制流图(controlflowgraph,CFG)为基础所构建的含序CFG结构.含序CFG是CFG的一种受限子集，它们的拓扑结构可映射为偏序集，这样诱导产生的自然数区间可自然地用于描述定义良好的程序结构.这种结构含有程序的静态结构信息和动态行为信息，换而言之，CFITL具有规约程序实现结构属性和程序执行动态行为属性的能力.在定义CFITL的语法和语义的基础上，详细讨论了CFITL的模型检验问题，包括基于值状态空间可达性计算的模型检验方法和基于SMT(satisfiabilitymodulotheories)的CFITL有界模型检验方法.现代程序都含有复杂且具有无限值域的抽象数据类型及各种复杂的操作，CFITL语义定义相比CTL等时序逻辑更复杂，因此，基于显示状态搜索的方法难以有效进行，而基于SMT的CFITL有界模型检验方法更易实现、更具有可行性.最近开发相关的原型工具，并进行相关的实例研究.

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