首页 | 本学科首页   官方微博 | 高级检索  
     

基于敏感位置识别的状态化简技术研究
引用本文:高洪博, 李清宝, 王炜, 朱瑜. 基于敏感位置识别的状态化简技术研究[J]. 电子与信息学报, 2013, 35(3): 742-748. doi: 10.3724/SP.J.1146.2012.00878
作者姓名:高洪博 李清宝 王炜 朱瑜
作者单位:解放军信息工程大学 郑州 450002
基金项目:国家863计划项目(2009AA01Z434)资助课题
摘    要:模型构建是模型检验的基础,在微控制器代码模型构建过程中面临状态爆炸的问题。由于生成模型的状态数量与代码规模密切相关,通过简化代码可以有效缩减生成的状态数量。该文提出了敏感变量和敏感位置的概念,并以此为基础提出了结合子程序摘要信息的敏感位置识别算法;该算法从待验证的性质出发,提取敏感变量,识别代码中与敏感变量相关的敏感位置;模型构建过程中只对敏感位置对应代码进行建模,从而实现对模型状态的缩减。实验结果表明所提的方法能够有效缓解微控制器代码模型生成过程中的状态爆炸问题。

关 键 词:模型检验;状态爆炸;敏感变量;敏感位置
收稿时间:2012-07-09
修稿时间:2012-12-04

The Study of State Simplification Techniques Based on Sensitive Position Identification
Gao Hong-Bo, Li Qing-Bao, Wang Wei, Zhu Yu. The Study of State Simplification Techniques Based on Sensitive Position Identification[J]. Journal of Electronics & Information Technology, 2013, 35(3): 742-748. doi: 10.3724/SP.J.1146.2012.00878
Authors:Gao Hong-bo Li Qing-bao Wang Wei Zhu Yu
Affiliation:PLA Information Engineering University, Zhengzhou 450002, China
Abstract:Model construction is the basis of model checking. State explosion can not be avoided during building model for microcontroller code. Because the state number of generated model is related to code size, the number of state can be reduced through simplifying microcontroller code. An algorithm of sensitive position identification with subroutine summary information is proposed, based on concepts of sensitive variable and sensitive position. Sensitive variables are extracted from verified properties and used to identify sensitive positions. Then model is constructed from code corresponding to sensitive positions. Experimental results show that the problem of state explosion can be effectively alleviated through the proposed method.
Keywords:Model checking  State explosion  Sensitive variable  Sensitive position
点击此处可从《电子与信息学报》浏览原始摘要信息
点击此处可从《电子与信息学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号