Software Verification For Sensor Network Based On Bounded Model Checking

Sensor network is a multiple-hop network which is formed by a kind of perception, processingand self-organizing sensor nodes. With the rapid development of sensor network, the scale ofsoftware increases gradually, that makes a higher requirements for software. Software verification isan important technology. Model checking is one of the software verification technologies; itprovides a new technical means for the sensor network software verification. The state spaceexplosion problem is bottleneck in the development of model checking. Bounded model checkingtechnology is a new research direction in the field of model checking, it is used for reducing thestate space explosion problem by limiting the number of states.This thesis presents a method based on bounded model checking, and it is described for thesource code. The implementation of this method is divided into two jobs:First of all, this thesis proposes a verified method for codes based on model checking, whichanalysis the static structure and dynamic behavior on the model, and defines the rules whichtransfers from model to C based on bounded model checking. Then we can do bounded modelchecking by CBMC for software verification in sensor network.Secondly, the thesis puts forward an improved POR (Partial-Order-Reduction) algorithm, whichbased on the model checking, the algorithm can avoid repeated path by using the method ofsegmentation on sensor network for software verification, the process of verification will beoptimized, and the experimental results show that it can improve the efficiency of sensor networkeffectively for software verification.