Applications of Wireless Sensor Networks (WSN) in harsh conditions usually cover a vast area with sensors randomly deployed by an uncontrolled method, e.g. dropped by helicopters. Thus the actual topology is unpredictable and can suffer from possible congestion. We propose the FCD framework for congestion detection, based on clustering techniques combined with Petri nets modelling and verification.
ns2 [
Petri Nets (PNs) are well-suited for modelling WSNs. To the best of our
knowledge, WSN-PN [
We adopt a Component-based PNs approach for modelling, which allows
convenient abstraction of components [
Petri net generation for a WSN: A WSN is defined as W SN = { S, C} , where S is the set of sensors and C is the set of channels. Sensors can be source, sink or intermediate nodes. A channel is established between two communicating sensors. Information on sensors and channels forms the topology of the WSN.
To build the corresponding PN model, sensors and channels are first modelled individually as Component PNs. Then, these Component PNs are combined together, forming the global model. For example, Fig. 1a models a source sensor.
It is also necessary to attach to transitions some code that manipulates the
quantitative values: sensor buffer size, sending rate and processing rate [
output generate packet send packet (a) Source node
S1
T1 in
T1 int T1 out T1 con T1 rec T1 send T2 con
S2
(b) Sensor abstraction model
Congestion detection: WSN-PN uses the PAT model-checker [
Congestion-oriented clustering: The clustering step groups the sensors with a high chance of congestion into clusters, using COCA. It operates according to two metrics: physical distance and imbalance of transmission rate of sensors, which are major congestion factors. The clusters generated by COCA are subnetworks with a high chance of congestion. The sensors not included in clusters are named abandoned sensors. For instance, Fig. 2a illustrates the clustering of a simple WSN. The three clusters C1, C2, C3 are pictured by ellipses. PN models of clusters and local verification: The clusters are considered as sub-WSNs and modelled using the Petri Net-based technique presented in Section 2. However, they miss important information such as source and sink sensors, e.g. in Fig. 2a, cluster C1 misses both source and sink.
If a cluster misses source/sink, external sensors are chosen to serve as auxiliary ones, such that: (1) the source is an external sensor that sends incoming packets to the cluster; (2) the sink is an external sensor that receives outgoing packets from the cluster. The original cluster C1 in Fig. 2b is replaced by Fig. 2c, i.e. both sensors S17 and S18 become sources while S20 becomes sink.
Each sensor being modelled by a PN, the size of whole PN model increase with
multiple sources/sinks. However, according to [
Abstracted clustered global models and verification: To limit state space explosion, clusters are abstracted, then composed together with the abandoned sensors. Congestion-less clusters are abstracted as “virtual” sensors. Dummy channels are created to mimic real channels. Finally, the PN model is generated and the congestion property verified.
S7 S10
S9 S11 S1 S4 (a) Clusters generated by COCA (b) Original cluster C1
S8 S18 S8 S18
S7 S9
S9
S10 S11 S10
S17 S17
S20
S20 (d) Abstraction of cluster C1
their intermediate sensors are removed while sensors with incoming/outgoing channels to/from the cluster are kept as well as sources and sinks. For example, abstraction of cluster C1 is shown in Fig. 2d. The inner arcs in the cluster are computed according to transmission rates, thus creating dummy channels that mimic the original behaviour.
Fig. 3: Abstracted network topology coming and outgoing packet rates. The incoming packet rate of a sensor si, denoted by In(si), is the total number of packets that are sent to sensor si. Its outgoing packet rate, denoted by Out(si), is the minimum value of the incoming packets rate of si and its processing rate, i.e. Out(si) = min(In(si), pr (si)).
A dummy channel cij is created between sensors si and sj if and only if there exists a path from si to sj . Its transfer rate, tr d(cij ) is the minimum value of { 20} S18 { 5} { 10} S7 outgoing packets of sensor sk and transfer rate tr (ckj), for all sensors sk along the path, i.e.: tr d(cij) = minsk∈ path(si,sj),sk0 =succ(sk) min(Out(sk), tr (ckk0 )).
Consider cluster C1 in Fig. 4a where the red numbers are the processing rates of sensors, and the blue ones the transfer rates of channels. Figure Fig. 4b illustrates the dummy channels creation when removing S7 and S11. The abstracted clusters and the remaining abandoned sensors lead to an abstracted network, as shown in Fig. 3. WSN-PN is used again to verify congestion on this new network.
FCD was experimented with WSNs modelled by WSN-PN under random topologies having 70 to 10, 000 sensors, as shown in Table 1. ification time of FCD is significantly reduced compared to WSN-PN. Topologies 1–6 have a dense deployment, and most sensors are grouped into clusters. The more the sensors, the longer the verification. In topologies 7–12, the WSNs are sparsely deployed. Even though most clusters are very small, congestion occurs in large ones. The last three cases do not allow for getting a result, due to the limitations of the WSN-PN tool, since the networks to verify are too large. 5
This paper presented FCD, a framework combining clustering technique and formal verification in order to efficiently find possible congestion in WSNs. WSNs are clustered based on the congestion-oriented measurement first. Then, the verification process is performed on each individual cluster. Congestion is detected earlier if it exists within a cluster. Otherwise, the verification process is repeated on a new abstracted network obtained from abstracted clusters and abandoned sensors in case clusters are confirmed congestion-free in the previous step. Experiments show that in most cases, congestion is detected on clusters, which significantly decreases the verification time.