Formal approaches to wireless sensor networks

Wireless sensor networking, as a burgeoning technology, supports the monitoring of physical environments and control of sensor data, and has been widely applied in many fields. Due to its unique features, a number of formal theories, as well as verification tools, have been developed to make an in-depth study. In this paper, we propose a timed broadcasting language, the Timed Wireless Sensor Processes, with its operational semantics borrowing ideas from both the Timed CSP and the CBS. Moreover, we abstract a model of contention-based wireless sensor networking systems and formalize it using our language. We also simulate real-world scenarios in terms of labeled transition systems to demonstrate our methods in describing the dynamic behaviors of wireless systems.