Wireless sensor networks may be used to conduct critical tasks like fire detection or surveillance monitoring. It is thus important to guarantee the correctness of such systems by systematically analyzing their behaviors. This task is extremely challenging as the state space of sensor networks is huge, e.g., due to interleaving of sensors and intra-sensor interrupts. In this work, we develop a method to reduce the state space significantly so that state space exploration methods (like model checking or systematic testing) can be applied to a much-smaller state space without missing a counterexample. Our method explores the nature of networked NesC programs and uses a novel two-level partial order reduction approach to reduce both interleaving among sensors and intra-sensor interrupts. Applying partial order reduction for sensor network programs is highly non-trivial, due to the interplay between inter-sensor message passing and interrupts or among interrupts. We define systematic rules for identifying dependence at sensor and network levels so that partial order reduction can be applied effectively. We have proved the soundness of the proposed reduction technique, and present experimental results to demonstrate the effectiveness of our approach.

• Technical Report: a detailed report of our POR approach with proofs for all related theorems. Download the report here.
• Experiment materials: more detailed experiment results, with links for downloading case studies and a guide for running experiments, could be found here.
• Information about NesC@PAT : click here.

In the following, we will present two case studies. All necessary materials for re-running the experiments are also provided.

• Anti Theft
  Anti-theft is taken from the TinyOS distribution, which represents a real-world application of sensor networks. This applications consist of more than 3000 LOC of the NesC program running on each sensor.
  
  
• Trickle
  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.

• Run experiments with NesC@PAT


1. System requirements:
   For Windows OS: Windows Operating System: Windows XP, Vista, Windows 7 and Windows Server 2000/2003. .NET Framework 3.5 is needed to run NesC@PAT, which can be downloaded here.
   For Linux, Mac OS and others: Mono 2.6.7 or later.
   
   
2. Download the latest executable NesC@PAT here.
   For Windows OS, just unzip and click PAT.exe for execution.
   
   For Linux, Mac OS and others, please follow these steps:
   
   • Unzip "NesCatPatPor.zip".
   • Install MONO tool in your system: you should install mono tool in your system which is freely available. Please download from here according to your OS. Note that libmono-winforms2.0-cil (plus its dependencies) may need be added in order to run PAT under Linux (Ubuntu).
   • In your computer, start terminal application, using the command cd to the directory where you unzip "NesCatPatPor.zip".
   • Type the command mono "PAT 3.exe" into terminal.(You might need to add execute permission as chmod +x "./PAT 3.exe" ) Bingo! You will see the GUI of our PAT.
   
   
3. Download source files for the examples zip file here, and then unzip the examples.
   
   
   
4. Run Experiments
   
   • GUI Mode
   1. In PAT GUI, click "File -> Open" and open the "*.sn" files in the example folder.
   2. Confiture parameters for verification:
      
   Click "Tools -> Options -> NesC Model"
   (1) For Trickle application:
   - Start from Default Setting (by clicking the button "Default Setting");
   - Set the Buffer Size as 2. (This is important, otherwise the model will be wrong because of serious message loss problem.)

   (2) For AntiTheft application: Default Setting will do (by clicking the button "Default Setting").

   (3) For both cases: If you want to simulate a sensor network with POR, click the checkbox of "Simulating with POR".

   3. Verify sensor networks:
   
   Click the button "Verification" or "F7" to open the Verification window.
   
   (1) For safety properties (e.g., deadlock-freeness or error state reachability), choose the third or fourth Verification Engine, which is either "First Witness Trace with Partial Order Reduction" or "Shortest Witness Trace with Partial Order Reduction".
   
   (2) For linear temporal properties, choose the second Verification Engine "Strongly Connected Component Based Search with POR".
   
   
   • Batch Mode (only works for Windows OS)
     Download the batch file here and save it in the NesC@PAT root folder, then execute the batch file. Results will be documented in the Results folder in the same folder.
     
     
• Run experiments with T-Check
1. Install T-Check, following Steps 1 - 3 of the instructions shown here.
2. Download TrickleExample.zip, unzip and put it in TinyOSROOT/apps (TinyOSROOT: the path where you install your TinyOS).
3. Run Trickle test cases

$cd TinyOSROOT/apps/TrickleExample
$./preprocessing TRICKLEPROPERTY "$1/propertyWiring.txt"
$make micaz sim
$chmod 755 ./runTasks.sh
$exec ./runTasks.sh


4. The results will be stored in a number of files named with "StatiticData_m_n_mode.txt" in the same path.

• Results of NesC@PAT with Two-Level POR



App	Property	Meaning	Size	Result	#State	#Trans	Time(s)	Overhead (ms)	#States wo POR	POR Ratio
Anti Theft	Deadlock Free	Deadlock is absent.	3	✓	1.2M	1.2M	791	95	>2.3G	< 6 × 10-4
	□(theft ⇒ ◇alert)	Whenver a theft is detected, the alert led is turned on.		✓	1.3M	1.4M	2505	108	>4.6G	< 3 × 10-4
Trickle	◇ AllUpdated	Eventually all sensor nodes are updated with the newest code in the network.	2	✓	3268	3351	3	2	111683	3 × 10-2
			3	✓	208K	222K	74	3	12M	< 8 × 10-4
			4	✓	838K	947K	405	4	>1.6G	< 2 × 10-4
			5	✓	13.3M	15.7M	8591	5	>320G	< 1 × 10-4
	Never FalseUpdate	Each node never updates its code with an older version.	2	✓	3012	3081	0.8	2	52324	6 × 10-2
			3	✓	120K	124.2K	20	3	>11.8M	< 1 × 10-2
			4	✓	368K	384K	58	4	>2.7G	< 1 × 10-4
			5	✓	4.2M	4.4M	638	5	>61.6G	< 7 × 10-6


The meaning of each column is illustrated as follows:

• App: the name of application being checked.
• Property: the property to be checked.
• Meaning: the meaning of the corresponding property.
• Size: the network size, i.e., number of sensor nodes.
• Result: verification result, i.e., if the property is valid.
• #State: number of states using POR.
• #Trans: number of transitions using POR.
• Time(s): time (in seconds) used using POR.
• Overhead(ms): the additional time used for static analysis at compile time, in milliseconds.
• #States wo POR: number of states without POR.
• POR Ratio: POR Ratio = (#State)/(#States wo POR), is the reduction ratio gained by the two-level POR.
• Results of T-Check in the perspective of POR performance
  

T-Check is a model checker for TinyOS applications, which uses DFS or random walk to explore the system space of a sensor network to find a violation of a given property. In the following, we present the experimental results of checking the Trickle algorithm for the safety property Never FalseUpdate.



#Node	#Bound	#State	Exh	Time(s)	#State wo POR	POR Ratio
2	20	4765	Y	1	106.2K	≈ 4 × 10-2
3	12	66.2K	N	1	12.5M	≈ 5 × 10-3
	50	12.6M	Y	283	NA	NA
4	10	56.7K	N	1	41.8M	≈ 1 × 10-3
	50	420.7M	Y	1291	NA	NA
5	8	85.2K	N	1	17.4M	≈ 1 × 10-3
	50	NA	N	>12600	NA	NA




The meaning of each column is illustrated as follows:

• #Node: the network size, i.e., number of sensor nodes.
• #Bound: the bound number used for DFS.
• #State: number of states using POR.
• Exh: if the whole system space is exhaustively explored: Y= yes, N = no.
• Time(s): time (in seconds) used using POR.
• #State wo POR: number of states without POR.
• POR Ratio: POR Ratio = (#State)/(#States wo POR), is the reduction ratio gained by the POR of T-Check.
  
  
• Comparison and Discussion