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

摘要

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