@inproceedings{c9ba63b1493c443f91e6d5b2860eeae6,
title = "Sensor checker: Reachability verification in mission-oriented sensor networks",
abstract = "This paper presents novel techniques to verify the global reachability in mission-oriented wireless sensor networks (Mission-Oriented WSN). The global reachability verification considers configurations such as forwarding information and awake/dormant schedule as generated by WSN protocols and algorithms. Our contribution is two-fold. First, we create a scalable model that represents the end-to-end reachability of WSN based on node configuration using Binary Decision Diagrams (BDDs) and Symbolic Model Checking, and then define generic reachability properties using Computational Tree Logic (CTL). Second, we encode the Mission-Oriented WSN topological information using Boolean functions to verify constraint-based reachability properties for WSN, and show soundness and completeness. We implement this in a tool called SensorChecker. The scalability and performance of SensorChecker is validated with very large WSN networks (10s of thousand of nodes) and wake-up scheduling parameters. To the best of our knowledge, this is the first formal approach for verifying large-scale WSN network configuration.",
keywords = "Computational tree logic, Model checking, Reachability, Verification",
author = "Ehab Al-Shaer and Qi Duan and Saeed Al-Haj and Moustafa Youssef",
year = "2013",
doi = "10.1145/2509338.2509344",
language = "English",
isbn = "9781450323673",
series = "Proceedings of the Annual International Conference on Mobile Computing and Networking, MOBICOM",
pages = "51--56",
booktitle = "MiSeNet 2013 - Proceedings of the 2nd ACM Annual International Workshop on Mission-Oriented Wireless Sensor Networking",
note = "2nd ACM Annual International Workshop on Mission-Oriented Wireless Sensor Networking, MiSeNet 2013 ; Conference date: 04-10-2013 Through 04-10-2013",
}