Petri net-based parallel model checking with a splitting procedure
Muhammad Syafiq Bin Ab Malek, Mohd Anuaruddin Bin Ahmadon, Shingo Yamaguchi · 2015
Model checking is very important to analyse the behavior of consumer electronic products. However, if a product has large-scale behavior, we cannot use model checking because of state space explosion. In this paper, we propose a Petri net-based framework of parallel model checking and a Petri net splitting procedure. The proposed framework is useful to reduce the size of the net, thereby increases the applicability of model checking. This parallel model checking allows us to analyse the property of each splitted nets simultaneously. We illustrate the proposed framework with a product called as i-Refrigerator as an application example.