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:

deb tested on Ubuntu

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:

deputy tested on Ubuntu

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.

make micaz (safe) sim
make micaz (safe) sim-sf
make micaz (safe) sim-fast

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.

In addition, if the safety violation is the memory safety violation triggered by deputy assertion-like checks, T-Check will also output the verbose bug information into a file named "BugFile.txt".
If the deltaDebugging option is set, then T-Check will automatically shorten the buggy trace and dump it.

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

If the critical transition is found, then a trace starting from initial state to critical transition will be dumped,
Otherwise, the whole trace is dumped to uses to make them inspect the execution. These two kinds of traces are both preserved into a file named "LiveViolating%d.txt" where %d denotes the number of current path in the same manner as safety violating file.