Study on Modularized Model Checking Method Based on SPIN

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.