A Formal Co-Simulation Approach for Wireless Sensor Network Development

Abstract

This paper proposes a Formal Co-simulation (FoCoSim-WSN) framework to provide a good software engineering practice for wireless sensor networks (WSNs) including high-level abstraction, separation of concerns, strong verification and validation (V&V) techniques. This provides an iterative interworking framework  which combines the benefits of existing simulation and proof-based formal verification approaches. The complexity of software development for the sensor node controller is reduced by separating the controller model from the simulation environment. Controller algorithms from application through network and MAC layers can be formally developed and verified in a layered manner using the refinement method of the Event-B language and its RODIN toolkit. The absence of certain classes of faults in controller models which cannot be guaranteed by simulation testing techniques, can be proved by formal methods. On the other hand, the MiXiM simulation of physical environment provides full confidence about reliability and performance analysis through long running simulation via wireless channels.  Our prototype development confirms the flexibility of the framework for interworking between formal, simulation and co-simulation modelling.