|
|
|
| The Study of State Simplification Techniques Based on Sensitive Position Identification |
| Gao Hong-bo Li Qing-bao Wang Wei Zhu Yu |
| 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.
|
|
Received: 09 July 2012
|
|
|
|
Corresponding Authors:
Gao Hong-bo
E-mail: ghb912@163.com
|
|
|
|
|
|
|
2013, Vol. 35 
