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

作者：霍玮; 李丰; 丁兆伟; 桑春雷; 张兆庆; 冯晓兵

来源：计算机学报, 2012, (02): 2244-2256.

• 有限状态自动机
• 时序安全属性
• 切片技术
• 程序静态检测
• F-衡量 finite state machine
• temporal safety property
• slicing
• static program checking
• F-measure

程序时序安全属性可以用有限状态自动机(FSM)来描述,对该属性的静态检测是当前研究的热点之一.该文提出了FSM切片技术,以需求驱动的模式抽取出关于时序安全属性等价的程序切片.该切片使检测规模减小、程序结构简化,因而减小了检测中组合爆炸情形出现的机会,最终使时序安全属性的静态检测在准确性和可伸缩性上都得到了提高.实验表明,FSM切片可以使Saturn的可伸缩性平均提高到原来的6.34倍,使Fastcheck的准确性平均提高到原来的1.20倍.

• 单位
  中国科学院研究生院; 计算机体系结构国家重点实验室; 中国科学院计算技术研究所