陈冬火　刘　全,2　金海东　朱　斐,2　王　辉

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



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

陈冬火1刘全1,2金海东1朱斐1,2王辉1

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

(dhchen@suda.edu.cn)

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

区间时序逻辑; 控制流程图; 程序静态结构；……