摘要
程序时序安全属性可以用有限状态自动机(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.
出处
《计算机学报》
EI
CSCD
北大核心
2012年第2期244-256,共13页
Chinese Journal of Computers
基金
国家"八六三"高技术研究发展计划项目基金(2008AA01Z115)
国家自然科学基金青年科学基金项目(61100011)
国家自然科学基金创新研究群体科学基金项目(60921002)
国家"核高基"重大专项基金项目(2009ZX01036-001-002)
国家"九七三"重点基础研究发展规划项目基金(2011CB302504)资助~~