基于敏感位置识别的状态化简技术研究

模型构建是模型检验的基础，在微控制器代码模型构建过程中面临状态爆炸的问题。由于生成模型的状态数量与代码规模密切相关，通过简化代码可以有效缩减生成的状态数量。该文提出了敏感变量和敏感位置的概念，并以此为基础提出了结合子程序摘要信息的敏感位置识别算法；该算法从待验证的性质出发，提取敏感变量，识别代码中与敏感变量相关的敏感位置；模型构建过程中只对敏感位置对应代码进行建模，从而实现对模型状态的缩减。实验结果表明所提的方法能够有效缓解微控制器代码模型生成过程中的状态爆炸问题。

The Study of State Simplification Techniques Based on Sensitive Position Identification

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.