Formal verification of real-time wireless sensor networks protocols with realistic radio links
Alexandre Mouradian, Isabelle Augé-Blum · 2013
Many critical applications which rely on Wireless Sensor Networks (WSNs) are proposed. Forest fire detection, landslide detection and intrusion detection are some examples. Critical applications require correct behavior, reliability, and the respect of time constraints. Otherwise, if they fail, consequences on human life and the environment could be catastrophic. For this reason, the WSN protocols used in these applications must be formally verified. Unfortunately the radio link is unreliable, it is thus difficult to give hard guarantees on the temporal behavior of the protocols (on wired systems the link error probability is very low [7], so they are considered reliable). Indeed, a message may experience a very high number of retransmissions. The temporal guarantee has thus to be given with a probability that it is achieved. This probability must meet the requirements of the application.