一种提高时序安全属性静态检测实用性的方法  

A Precise and Scalable Static Checking Approach for Temporal Safety Property

作　　者：霍玮[1] 李丰[1,2] 丁兆伟[1] 桑春雷[1,2] 张兆庆[1] 冯晓兵[1] 

机构地区：[1]中国科学院计算技术研究所计算机体系结构国家重点实验室,北京100190 [2]中国科学院研究生院,北京100049

出　　处：《计算机学报》2012年第2期244-256,共13页Chinese Journal of Computers

基　　金：国家"八六三"高技术研究发展计划项目基金(2008AA01Z115);国家自然科学基金青年科学基金项目(61100011);国家自然科学基金创新研究群体科学基金项目(60921002);国家"核高基"重大专项基金项目(2009ZX01036-001-002);国家"九七三"重点基础研究发展规划项目基金(2011CB302504)资助~~

摘　　要：程序时序安全属性可以用有限状态自动机(FSM)来描述,对该属性的静态检测是当前研究的热点之一.该文提出了FSM切片技术,以需求驱动的模式抽取出关于时序安全属性等价的程序切片.该切片使检测规模减小、程序结构简化,因而减小了检测中组合爆炸情形出现的机会,最终使时序安全属性的静态检测在准确性和可伸缩性上都得到了提高.实验表明,FSM切片可以使Saturn的可伸缩性平均提高到原来的6.34倍,使Fastcheck的准确性平均提高到原来的1.20倍.Static program checking on temporal safety property that can be described by finite state machine （FSM） has been one of the hot research topics recently. In this paper, we propose a new approach to improve both of the precision and scalability of static program checking. We used FSM slicing to reduce the size of the programs being checked in a demand driven manner without checking precision loss. Such reduction can simplify the structure of the programs thus reduce the complexity of the program analysis used by the program checking. The experiment results show that the FSM slices can improve the scalability of the Saturn to 6.34 times on average, and can improve the precision of the Fastcheck to 1.20 times on average.

关 键 词：有限状态自动机 时序安全属性 切片技术 程序静态检测 F-衡量 

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