Real-Time Logic Verification of a Wireless Sensor Network

Monitoring and control of systems using a wireless sensor network (WSN) play a significant role in rapid automated response to events. Automation drives the necessity to check the system correctness due to the critical nature of the operations (i.e. military, air traffic management). The motes in a WSN are event-driven systems. The evolution of the system can be captured by discrete and continuous dynamics modeled using hybrid systems. This leads to the development of a trajectory, allowing for verification of logical correctness that responds to dynamics. We propose a formal modeling paradigm using temporal logics to verify the system, developed modularly as a set of interacting hybrid automata. The method formulates the specifications and checks for satisfaction. The models are implemented using UPPAAL, a real time verification tool.