程序条件化用于软件模型检测中的状态空间缩减.pdf

第 40 卷 　第 4 期 西 　安 　交 　通 　大 　学 　学 　报 Vol . 40 　№4 2006 年 4 月 　　 　 Ap r . 2006 J OU RN AL O F XI′AN J IA O TON G U N IV ER SI T Y 程序条件化用于软件模型检测中的状态空间缩减 1 ,2 1 1 3 肖健宇 , 张德运 , 郑卫斌 , 张 　勇 ( 1. 西安交通大学电子与信息工程学院 , 7 10049 , 西安 ; 2 . 邵阳学院激光与信息研究所 , 422000 , 湖南邵阳; 3 . 西安安智科技有限公司 , 7 10049 , 西安) 摘要 : 针对软件模型检测中的状态爆炸问题 ,提出将程序条件化技术用于软件状态空间缩减的方 案. 以程序性质的线性时序逻辑公式可能出现的蕴涵式的前件作为条件化的约束条件 ,通过分析程 序符号化执行语义 ,借助自动定理证明器 ,对语句的可达性条件进行逻辑推理 ,删除那些与性质的 可满足性无关的语句 , 以达到程序精简的目的. 理论分析和实验结果表明 ,条件化可以有效缩减程 序状态空间 ,而且缩减后的程序模型保留了原程序中与所需验证的性质有关的所有信息 ,满足软件 模型检测对状态缩减的安全性要求. 关键词 : 程序条件化 ;软件模型检测 ;状态空间缩减 ;符号化执行 ;线性时序逻辑 ( ) 中图分类号 : TP3 11 1 　文献标识码 : A 　文章编号 : 0253987X 2006 Applying Program Conditioning to Reduce State Space f or Sof t ware Model Checking Xiao J ianyu1 ,2 , Zhang Deyun1 , Zheng Weibin1 , Zhang Yong ( 1. School of Elect ronics and Infor mation Engineering , Xi ′an J iaotong U niver sit y , Xi ′an 7 10049 , China ; 2 . In stit ut e of L a ser and Infor mation , Shaoyang College , Shaoyang 422000 , Hunan , China ; 3 . Xi ′an Anzhi Science and Technology Lt d . , Xi ′an 7 10049 , China) Abstract : Aiming at t he st at e exp lo sion p roblem exi st ed in t he soft ware mo del checking , a