NesC@PAT: A Model Checker for Sensor Networks

  • Updates of NesC@PAT

    • Our paper on the two-level Partial Order Reduction for sensor networks is presetned in VMCAI 2013, Rome, Italy. Jan 22, 2013.
    • Two-level Partial Order Reduction for sensor networks is implemented. Mar 15, 2012.
      Details could be found here.
    • NesC@PAT is presented in ICFEM 2011, Durham, UK. Oct 29, 2011.

    Download NesC@PAT here. Note that you need to register before downloading it.

  • Introduction
  • Sensor networks are usually expected to perform critical tasks unattendedly for a long period, thus it is important to verify their reliability and correctness. The state-of-the-art programming language and platform of sensor networks, NesC [1] and TinyOS [2],adopt the low-level programming style. Although such designs are able to provide fine-grained control over the underlying resource constraints, they are difficult for human to comprehend, maintain, debug and verify sensor network applications. NesC@PAT is a module developed in the model checking toolkit PAT [3] specifically for sensor networks. NesC@PAT is developed for automatic modeling and verifying sensor networks running TinyOS applications implemented in NesC.

  • - Technical Report [pdf]: details of the underlying theoretic and techincal principals of NesC@PAT (including the formal semantics of NesC and sensor networks).

    - User Manual: a detailed document on how to build a sensor network in NesC@PAT for modeling and verification, including:

    1. Drawing a sensor network;
    2. Defining verfication goals (assertions);
    3. Simulating and verifying a Blink application.

  • Trickle [4] is a code propagation algorithm intended to reduce network traffic. Trickle controls message sending rate so that each sensor hears a small but enough number of packets to stay up to date. Each sensor periodically broadcasts its code summary, and
            - stays quiet if receiving an identical code summary;
            - broadcasts its code if receiving an older summary;
            - broadcasts its code summary if receiving an newer summary.

    NesC@PAT has been used to verify the Trickle algorithm of sensor networks and a bug is detected, which has been confirmed with real execution on real sensors. The source code for experiments and videos of real execution on real sensors are presented.

    1. Verifying Trickle with NesC@PAT

      • Implementing Trickle in NesC
      • Modeling sensor networks of Trickle with different topologies
      • Definining Properties for verifications
      • Verification Results
      • Discussion and Evaluation

      Expand >>>

    2. Executing Trickle on real sensors

      • Adding operations on leds
      • Configuring network topology
      • Videos of Real Executions

      Expand >>>

  • Reference

    1. D. Gay, P. Levis, R. v. Behren, M. Welsh, E. Brewer, and D. Culler. The nesC Language: A Holistic Approach to Networked Embedded Systems. In PLDI, pages 1 - 11, 2003.
    2. P. Levis and D. Gay. TinyOS Programming. Cambridge University Press, 1 edition, 2009.
    3. Y. Liu, J. Sun, and J. S. Dong. An Analyzer for Extended Compositional Process Algebras. In ICSE Companion, pages 919 - 920. ACM, 2008.
    4. P. Levis, N. Patel, D. E. Culler, and S. Shenker. Trickle: A Self-Regulating Algorithm for Code Propagation and Maintenance in Wireless Sensor Networks. In NSDI, pages 15 - 28, 2004.

    This page is maintained by Manchun Zheng.