《计算机学报》文章摘要   全文下载
  文章题目一种提高时序安全属性静态检测实用性的方法
  作者霍玮1) 李丰1),2) 丁兆伟1) 桑春雷1),2) 张兆庆1) 冯晓兵1)
  作者单位1)(中国科学院计算技术研究所计算机体系结构国家重点实验室 北京 100190) 2)(中国科学院研究生院 北京 100049)
  发表年份2012
  发表月份2期(244—256)
  文章摘要摘要 程序时序安全属性可以用有限状态自动机(FSM)来描述,对该属性的静态检测是当前研究的热点之一.该文提出了FSM切片技术,以需求驱动的模式抽取出关于时序安全属性等价的程序切片.该切片使检测规模减小、程序结构简化,因而减小了检测中组合爆炸情形出现的机会,最终使时序安全属性的静态检测在准确性和可伸缩性上都得到了提高.实验表明,FSM切片可以使Saturn的可伸缩性平均提高到原来的6.34倍,使Fastcheck的准确性平均提高到原来的1.20倍. 关键词 有限状态自动机;时序安全属性;切片技术;程序静态检测;F-衡量 中图法分类号 TP311 DOI号: 10.3724/SP.J.1016.2012.00244