State Space Reduction on Wireless Sensor Network Verification Using Component-Based Petri Net Approach

With the recent advancement of Internet of Things, the applications of Wireless Sensor Networks (WSNs) are increasingly attracting attention from of both industry and research communities. However, since the deployment cost of a WSN is relatively large, one would want to make a logic model of a WSN and have the model verified beforehand to ensure that the WSN would work correctly and effectively once practically employed. Petri Net (PN) is very suitable to model a WSN, since PN strongly supports modeling concurrent and ad-hoc systems. However, verification of a PN-modeled system suffers from having to explore the huge state space of the system. In order to overcome it, in this paper we suggest a novel component-based approach to model and verify a PN-modeled WSN system. First of all, the original WSN system is divided into components, which can be further abstracted to reduce the model size. Moreover, when verifying the corresponding PN model produced from the abstracted WSN, we introduce a strategy of component-based firing, which can reduce the state space significantly. Compared to typical approach of PN-based verification, our method enjoys an impressive improvement of performance and resource consuming, as depicted in our experimental results.