Modelling and symmetry reduction of a target-tracking protocol using wireless sensor networks

To achieve precise modelling of real-time systems stochastic behaviours are considered which lead towards probabilistic modelling. Probabilistic modelling has been successfully employed in wide array of application domains including, for example, randomised distributed algorithms, communication, security and power management protocols. This study is an improvement over our previous work, which was based on the probabilistic analysis of a cluster-based fault tolerant target-tracking protocol (FTTT) using only grid-based sensor nodes arrangement. Probabilistic modelling is chosen for the analysis of FTTT protocol to facilitate benefits of symmetry reduction in conjunction with modelling. It is believed that for the first time correctness of the simplified version of a target-tracking protocol is verified by developing its continuous-time Markov chain (CTMC) model using symbolic modelling language. The proposed probabilistic model of a target-tracking wireless sensor networks will help to analyse the phases of FTTT protocol on a limited scale with finite utilisation of time. There are three main contributions of this study; first consideration of synchronised events between the modules, second, random placement of sensor nodes is taken into account in addition to grid-based sensor node arrangement, third one is the reduction in state space size through symmetry reduction technique, which also facilitates to analyse a larger size network. Symmetry reduction on Probabilistic Symbolic Model (PRISM) checker models is performed by PRISM-symm and the generic representatives in PRISM (GRIP) tool. Modelling of FTTT protocol is proved better with the usage of PRISM-symm after comparing the results of PRISM model, PRISM-symm and GRIP.