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.
高洪博, 李清宝, 王炜, 朱瑜. 基于敏感位置识别的状态化简技术研究[J]. 电子与信息学报, 2013, 35(3): 742-748.
Gao Hong-Bo, Li Qing-Bao, Wang Wei, Zhu Yu. The Study of State Simplification Techniques Based on Sensitive Position Identification. , 2013, 35(3): 742-748.