Slede: Lightweight Specification and Formal Verification of Sensor Networks Protocols

These pages describe work carried out under the NSF grant CNS-0627354 on Specification and Verification Challenges for Security Protocols in Sensor Networks. The PI is Hridesh Rajan and much of the work is carried out by Youssef Hanna.

News

Mar 2009: Youssef's submission to ESEC/FSE 2009 accepted.

Jan 2009: Youssef's submission to the ICSE 2009 Research Demonstrations track accepted as informal demo.

Nov 2008: Eclipse plugin for Slede is available for download.

July 2008: Slede is available for download.

Dec 2007: Youssef's submission to the ACM Conference on Wireless Network Security (WiSec 08) accepted.

Sep 2007: Youssef's submission to the ESEC/FSE 2007 doctoral symposium accepted.

News Archive

Running Examples


1. Run Eclipse.

2. Click on Windows -> Open Perspective -> Other.

3. Choose TinyOS and then press OK.



4. Click on File -> Import.

5. Choose File System under TinyOS and then press Next.



6. Enter the location of one of the examples extracted from the downloaded Slede package.

Enter a project name.

Choose the pc option for the platform and then press Finish.



7. Errors displayed next to SensorM.nc file are due to a bug of the TinyOS plugin (not Slede plugin) for TinyOS ver 1.1.0. Compilation is not affected though.

Open the file of extension sld.



8. Any change and saving of the verificiation configuration file will trigger the model extraction and verification processes.

Once a violaion of property is detected (if there is any), refresh the folder of the protocol implementation to get the counterexample (in counterexample.txt file).