r framework Slede for automatic formal verification of sensor network security protocol implementations written in nesC . Slede does not require upfront model construction thereby significantly easing the task of sensor network developer. Instead, a skeleton model is automatically extracted from the nesC implementation of the security protocol. This extracted skeleton model is then automatically composed with intrusion models and desired network topologies to create a complete verifiable model.
Please use this reference,, I hope this will help you
D. Gay, P. Levis, R. von Behren, M. Welsh, E. Brewer, and D. Culler. The nesC language:A holistic approach to networked embedded systems. In PLDI ’03: Proceedings of the 2003 conference on Programming language design and implementation, pages 1–11, 2003
M. Younan, S. Khattab, and R. Bahgat, "An Integrated Testbed Environment for the Web of Things," in ICNS 2015-The Eleventh International Conference on Networking and Services, ISBN: 978-1-61208-404-6, Rome, Italy, May, 2015, pp. 69-78.