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.

Expand >>>

- What can be done in NesC@PAT?
   NesC@PAT is able to :

1. Model a sensor based on the NesC program running on it;
2. Model a sensor network composed by a number of sensors (with NesC implementations) and a certain topology;
3. Simulate a sensor or a sensor network graphically;
4. Verify either a sensor or a sensor network for checking deadlock freeness, state rechability, and temporal properties.

- Architecture of NesC@PAT:
   NesC@PAT is built with the architecture in the following figure:



There are five main components, i.e., Editor, Parser, Model Generator, Simulator and Model Checker. Editor allows users to specify a sensor with a certain NesC program and draw the network topology of a sensor network, as well as define assertions (i.e., verification goals). Parser is developed to compile corresponding input from the Editor, including NesC Parser, Network Parser and Assertion Parser. Model Generator generates sensor models based on input NesC program and the built-in Hardware Model Collection. Moreover, it generates sensor network models based on sensor models and the network topology. Both sensor models and network models are then passed to Simulator and Model Checker for graphical simulation and verification, respectively.

- What are the important features of NesC@PAT?
   The important features of NesC@PAT include:

• Direct verification on implementations. NesC@PAT works directly on NesC implementations, without user efforts on building (abstract) models before analyzing or verifying sensor networks. Manual construction of models of sensor networks is avoided, therefore it is very convenient to use NesC@PAT to verify sensor networks.
• Formal operational semantics of TinyOS applications. The firing rules of NesC structures are formally defined. New semantic constructs are introduced for modeling the interrupt-driven feature of the TinyOS execution model.
• Formalization of network behaviors. The labelled transition systems of sensor networks are defined, capturing the compositional behaviors and communications of individual sensors. This allows network-level concurrent errors to be detected.
• Abundant-property Verification. NesC@PAT supports verification of deadlock freeness, reachability and linear temporal logic formulas. This provides flexibility for verifying various properties of sensor networks like the correctness of a certain protocol.


<<< Fold





• Publications


• Manchun Zheng, David Sanán, Jun Sun, Yang Liu, Jin Song Dong and Yu Gu. State Space Reduction for Sensor Networks using Two-level Partial Order Reduction. The 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2013), pages 515-535, Rome, Italy, Jan 20 - 22, 2013. [pdf, bib, slides]
• Manchun Zheng, Jun Sun, David Sanán, Yang Liu, Jin Song Dong, Yu Gu. Demo: Towards Bug-free Implementations for Wireless Sensor Networks. The 9th ACM Conference on Embedded Networked Sensor Systems (Sensys 2011), pages 407-408, Seattle, WA, USA, Nov 1 - 4, 2011. [pdf, bib]
• Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu: Towards a Model Checker for NesC and Wireless Sensor Networks. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 372-387, Durham, United Kingdom, October 25-28, 2011. [pdf, bib, slides]


• Documentation

- 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.


• Case Study

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 >>>




• Implementing Trickle in NesC

We implemented the Trickle algorithm in a NesC program TrickleApp, with the modification that a sensor only broadcasts its code summary if it receives any newer summary. Here are the souce code of TrickleApp: TrickleAppC.nc, TrickleC.nc, TrickleH.h.

The struct MetaMsg is defined to encode a message packet with a code summary, and ProMsg is defined to encode a message with both code summary and the corresponding code. Initially, each node will broadcast its code summary to the network (i.e. a MetaMsg packet). If an incoming MetaMsg packet has a newer code summary, the sensor will broadcasts its code summary; if the received summary is outdated, the sensor will broadcasts a ProMsg packet with its code summary and code. An incoming ProMsg packet with a newer code summary will update the sensor's code summary and code accordingly.

The following DFA describes the behaviors of TrickleApp:




• Modeling sensor networks of Trickle with different topologies

We have studied sensor networks with different topologies for this algorithm, including star, ring, and single-tracked ring.

Star	Ring	Single-tracked Ring

The .sn files (i.e., the input of NesC@PAT)of these sensor networks are Star.sn, Ring.sn and SRing.sn (Click the links to download the files), respectively.

In each network, Sensor1 is assigned with TrickleNewApp (source files include: TrickleNewAppC.nc, TrickleNewC.nc, TrickleH.h). TrickleNewApp is identical to TrickleApp except that the initial code/summary in TrickleNewApp is 1/1 (which is up-to-date), while the initial code/summary in TrickleApp is 0/0 (which is out-of-date). Other sensors (Sensor2, Sensor3 and so on) are all assigned with TrickleApp.

• Definining Properties for verifications

We studied four interesting properties of these sensor networks, as listed in the following table.

The following two states are defined to describe properties:
#define  FUpdated   Sensor1.App.code == 0;
#define  AllUpdated  (Sensor1.App.code == 1 && Sensor2.App.code == 1 && Sensor3.App.code == 1);

Type	Property	Assertion in NesC@PAT	Meaning
Safety	Deadlock free	#assert SensorNetwork deadlockfree;	The system is free of deadlocks.
	State reachability	#assert SensorNetwork reaches FUpdated;	A state where the code is updated with an older version one.
Liveness	LTL formulas	#assert SensorNetwork |= <> AllUpdated;	Finally each node is updated with the newest code.
		#assert SensorNetwork |= []<> AllUpdated;	Each node is updated with the newest code infinitely often.



• Verification Results

The table bellow illustrates the results of verifying TrickleApp.

Experimental Results of Verifying TrickleApp with Different Topologies

Property	Network	Result	#States	#Transition	Time(s)	Memory(KB)
Deadlock Free	Star - 3	✓	300,332	859,115	55	28,418
	Ring - 3	✓	1,093,077	3,152,574	197	136,367
	SRing - 3	✓	30,872	85,143	5	25,885
	SRing - 4	✓	672,136	2,476,655	153	38,421
Reach false update	Star - 3	☓	300,332	859,115	57	39,981
	Ring - 3	☓	1,093,077	3,152,574	192	127,708
	SRing - 3	☓	30,872	85,143	5	20,033
	SRing - 4	☓	672,136	2,476,655	180	70,075
<>All nodes updated	Star - 3	✓	791,419	2,270,243	164	36,730
	Ring - 3	✓	2,127,930	6,157,922	444	102,180
	SRing - 3	☓	146	147	<1	34,706
	SRing - 4	☓	226	227	<1	34,436
[]<>All nodes are updated	Star - 3	✓	1,620,273	6,885,511	721	13,281,100
	SRing - 3	☓	146	147	<1	34,706
	SRing - 4	☓	226	227	<1	34,436
	SRing - 8	☓	746	747	<1	40,639
	SRing - 20	☓	4,126	4,127	2	124,252



• Discussion and Evaluation

The results show that the algorithm satisfies the safety properties, i.e., neither a deadlock nor a state of false update is evidenced in the complete state space. As for the liveness property, both ring and star networks work well, which means that each node in either network is able to be updated with the newest code. However, the single-trackedring network fails to update all nodes. The counterexample produced by our tool shows that only one sensor is able to be updated with the newest code. By simulating the counterexample in NesC@PAT, we can find that the reason of this bug. On one hand, the initially updated node A receives old code summary from node C thus broadcasting its code but only node B can hears it. On the other hand, after node B is updated it fails to sends its code summary to node C because node B never hears an older code summary. We also increased the number of sensors with the single-tracked ring topology, and the results remained the same. The .sn files for more nodes are available for downloading: SRing_4Node.sn, SRing_8Node.sn, SRing_20Node.sn.

<<< Fold



2. Executing Trickle on real sensors



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

Expand >>>

We ran the TrickleApp program was executed on real sensors, i.e., Iris motes, to study whether the bug detected by NesC@PAT could be evidenced in real executions.

• Adding operations on leds:
  The TrickleAppC was modified by adding operations on leds to display the changes of code, such that
  1. Initially sensor A has the new code and has its red led on, while sensor B and C have the old code and have their yellow leds on.
  2. When a sensor is updated with the new code, it turns on the yellow led and turns off other leds.
  
  
• Configuring network topology:
  Different topologies are achieved by specifying different AM id for each sensor's AMSender and AMReceiverC. In TrickleApp, two senders and two receivers are used to send and receive summary and code respectively. We refer to the sender and receiver for summary as SSender and SReceiver, and the sender and receiver for code as CSender and CReceiver.



Network Topology

Topology	Sensor	SSender	SReceiver	CSender	CReceiver
Ring	A	4	4	5	5
	B	4	4	5	5
	C	4	4	5	5
Star	A	4	6,8	5	7,9
	B	6	4	7	5
	C	8	4	9	5
Single-tracked Ring	A	4	8	5	9
	B	6	4	7	5
	C	8	6	9	7



• Videos of Real Executions:
  The results of the real execution shows that both the star and ring network are able to update all three nodes, but the single-tracked ring network fails to update one node, which confirms that the bug could be evidenced in reality.
• The STAR topology with 3 nodes:
  
All three nodes have their RED leds on finally. Source code for this experiment can be downloaded here.




• The ring topology with 3 nodes:
  
All three nodes have their RED leds on finally. Source code for this experiment can be downloaded here.




• The single-tracked ring topology with 3 nodes:
  
only two nodes have their RED leds on finally and one node fails to turn on its Red led. Source code for this experiment can be downloaded here.



<<< Fold



• 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.