Adding value to WSN simulation through formal modelling and analysis

Reliable verification and validation techniques are essential to the development of wireless sensor networks (WSNs) in safety-critical domains. This paper proposes a hybrid verification and validation approach integrating formal methods and simulation to increase the quality of WSN development. Simulation, like model checking, can demonstrate the presence of faults but not guarantee their absence. Some classes of faults such as safety property breaches and certain liveness breaches can be proved absent by the use of formal models and theorem provers. Our case study work which combines simulation with formal modelling and verification in Event-B demonstrates this in an environmental application from the SensorScope project. MintRoute, together with S-MAC protocol, is simulated with connectivity failure scenarios using the MiXiM simulation tool. The work indicates the iterative interworking between the formal and simulation methods that we seek.