|
|
|
| Study on Modularized Model Checking Method Based on SPIN |
| Li Xing-feng① Zhang Xin-chang②③ Yang Mei-hong②③ Yan Bao-ping① |
①(Computer Network Information Center, Chinese Academy of Sciences, Beijing 100190, China)
②(Shandong Computer Science Centre, Shandong Academy of Sciences, Jinan 250014, China)
③(Shandong?Provincial?Key Laboratory of Computer Networks, Jinan 250014, China) |
|
|
|
|
Abstract To address the state explosion problem in the procedure of model checking, this paper proposes a SPIN- based modularized model checking method. The proposed method divides the original abstraction model into some modules, and verifies all the divided modules, instead of verifying the original model. In the dividing process, the semantic of original model can be completely included in the modules, and no semantic is added in the process. Consequently, the original model passes the verification of model checking if and only if all the modules pass the verification. The theoretical and experimental results show that the proposed method is valid.
|
|
Received: 15 July 2010
|
|
|
|
Corresponding Authors:
Zhang Xin-chang
E-mail: zhangxc@keylab.net
|
|
|
|
|
|
|
2011, Vol. 33 
