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.
李兴锋, 张新常, 杨美红, 阎保平. 基于SPIN的模块化模型检测方法研究[J]. 电子与信息学报, 2011, 33(4): 902-907.
Li Xing-Feng, Zhang Xin-Chang, Yang Mei-Hong, Yan Bao-Ping. Study on Modularized Model Checking Method Based on SPIN. , 2011, 33(4): 902-907.
2011, Vol. 33 
