Survivability Evaluation Of Wireless Sensor Network Based On Stochastic Model Checking

Wireless sensor networks are deployed in the region to monitor a large number of sensor nodes with wireless communication and collaboration capabilities autonomy composed of a multi-hop ad hoc networks. Impossible to detect and block all network intrusion, in most cases, it must ensure that in the event of invasion of the key facilities to provide uninterrupted service. Survivability officially born for this key service support technology. In order to clarify the network system in the event of a fault and whether the attack has the ability to continue to provide critical services, we need to assess the survivability, in order to be survival of the network design and deployment guide.Stochastic model checking technology is a finite state system verification technology, through the establishment of appropriate state of the system model to describe the system to be verified using formal logic equations nature of the Statute to be verified, and then call the automated analysis to verify completion of the nature of the algorithm. Stochastic model checking highly automated features gained wide acceptance and application in the analysis of system reliability, security, and other indicators.Stochastic model checking technology is fast, reliable, easy to use and so on, this article will use the stochastic model checking techniques to analyze the wireless sensor network survivability, the main work in the following three aspects:(1) The establishment of a continuous-time Markov chain model in a single node failure and aggressive behavior evolution, by combination of single-node model behavior establish a continuous-time behavior of the entire network evolution Markov chain model. The network model can characterize the relationship between communication nodes, avoiding the prior art model-based analysis of the dependence on the distribution of nodes and topology.(2) PRISM is the most advanced model of random testing tools, testing tools using PRISM model requires users to have a certain knowledge of concurrent systems,and workers in the field of wireless sensor networks is relatively lacking, so thedevelopment of the initial deployment of the network map survivability as a PRISM evaluation model modeling language to describe an algorithm, so as to achieve the purpose of the modeling process automation.(3) In order to quantify the network system to continue to provide critical services in the event of failure and attack, this paper established various continuous random logic CSL portray survivability assessment indicators, including k-connectivity probability, steady-state availability, and so on. We are above the model described in survivability and indicators CSL formula input PRISM, to complete the evaluation index can survive automated calculations. This application logic evaluation index described manner, so that we can focus only on the index itself,without concern for the calculation process to obtain values for the indicator.