T-Check: Bug Finding for Sensor Networks

What's T-Check?

T-Check, settled on TOSSIM as a suitable basis, is designed to stress TinyOS kernel or applications to make these sorts of problems reveal themselves prior to deployment. T-Check exploits both explicit state model checking and random walks to find bugs in sensor network applications running on TinyOS. T-Check offers users a good value proposition: by exploiting safety checks inserted by Safe TinyOS, users can find bugs without any extra annotation effort. However, if users provide additional, higher level safety and liveness properties, these can also be checked. User-specified properties may be in terms of a single node (e.g., "packets are eventually receive") or in terms of the entire network (e.g., "eventually, all nodes are part of the routing tree").

T-Check builds upon two basis: Safe TinyOS for memory safety, and the TOSSIM simulator. Safe TinyOS uses Deputy to guarantee the memory safety of TinyOS applications. TOSSIM is an event-driven simulator for networks of nodes running TinyOS.

Alike TOSSIM, T-Check works on Micaz platform.

Install T-Check

1. Install customized nesC compiler

The easiest way is to install our pre-compiled package, which can be download from here:

Or you can compile from the source by following the steps below (Prefered way):

  • (1). download the source code:
  •      cvs -d:pserver:anonymous@nescc.cvs.sourceforge.net:/cvsroot/nescc login
         cvs -z3 -d:pserver:anonymous@nescc.cvs.sourceforge.net:/cvsroot/nescc co -P nesc
      

  • (2). download the patch and
  •    cd nesc
       patch -p0 < nesc-tcheck.patch
      

  • (3). then follow the standard make process: bootstrap, configure, make and make install
  • 2. Install Deputy compiler

    Currently we only provide pre-compiled package:

    This pre-compiled package is same with the one included in the standard TinyOS toolchain, if installed that already, you can skip downloading here. After the installation, please overwrite the header file checks.h (/usr/lib/deputy/include/deputy) with this new checks.h

    3. Patch TinyOS

  • download TinyOS from the CVS
  •      cvs -d:pserver:anonymous@tinyos.cvs.sourceforge.net:/cvsroot/tinyos login
         cvs -z3 -d:pserver:anonymous@tinyos.cvs.sourceforge.net:/cvsroot/tinyos co -P tinyos-2.x
       

  • then download our patch for T-Check
  •      cd tinyos-2.x
         patch -p0 < tcheck-20100709.patch (This patch can fit the latest TinyOS on 2010.07.09)
       
    After preparing the nesC compiler, deputy compiler and T-Check toolchain successfully, the user can start running applications.

    4. How to run applications in T-Check?

    4.1 How to add safety annotation and write high-level properties?

  • Please refer to Deputy Manual and Safe TinyOS to learn how to add safety annotations. Moreover, users may also learn from some T-Check applications with plenty of added annotations, such as CTP, DIP, or 6lowpan.
  • Please refer to here to learn how to wire property components into compilation and write executable properties via preprocessing perl script.
  • 4.2 How to configure Makefile?

    After adding necessary annotations and writing the high-level properties, users should add some necessary flags into application Makefile manually to make T-Check execute normally.

    4.3 How to write python script?

    Please also refer to here to write python script.

    4.4 How to compile toolchain and run applications?

    We made efforts to reduce the cost to develop applications with T-Check. Basically, the operation on T-Check is similar to that on Tossim. After preparing the python program, users can use following commands to compile the whole T-Check toolchain.

    safe means the compiling and running in safe mode. After compilation, users can use "python xxx.py" to drive the T-Check.

    And download a sample application for MultihopOscilloscope including preprocessor perl script and give a try.

    Note that users should set the environment variables according to their own situations

    4.5 How to analyze the result?

    During the running, If a T-Check-enabled application encounters a safety violation, it will dump an execution trace leading to the violation, and this trace is preserved into a file named "SafetyViolating%d.txt" where %d denotes the number of current path.

    If a liveness violation is found, T-Check searches for the critical transition