Component-Based Abstraction of Petri Net Models
Khanh Le, Thang Hoai Bui, Tho Quan, Laure Petrucci, Étienne André · 2015
This paper proposes a new approach for modelling a Congestion Detection mechanism on Wireless Sensor Networks (WSN) using the Petri Net (PN) language. Even though PNs are powerful for modelling concurrent systems, they suffer from a high computational cost when verifying properties on the modelled system. We suggest a component-based abstraction to tackle this problem. First, a PN system can be considered as a set of connected components. For instance, a WSN includes a Sensor component and a Channel component. When performing verification on a model, we can abstract the insignificant components and only focus on the remaining ones. Experiments demonstrate that our approach is practically feasible when tested with various kinds of congestion occurring on different PN modelling WSNs.