Please use this identifier to cite or link to this item:
Title: Systematic and automatic verification of sensor networks
Keywords: Sensor Networks, Formal Verification, Partial Order Reduction, Cartesian Semantics, TinyOS, NesC
Issue Date: 22-Jan-2013
Source: ZHENG MANCHUN (2013-01-22). Systematic and automatic verification of sensor networks. ScholarBank@NUS Repository.
Abstract: We investigate how software verification techniques could be adopted to systematically model check SNs implemented in NesC/TinyOS, which is one of the most widely used platforms for developing SNs. Firstly, we translate a NesC program to a semantically equivalent specification in Stateful Timed CSP (STCSP), and hence model checkers for STCSP like PAT can be used to formally verify the NesC program. Then, we develop the direct verification approach so that the capability of revealing errors/bugs could be maximized. The complete semantics of SNs is defined as a set of 66 firing rules. Model checking algorithms are developed to verify SNs against safety properties and liveness properties. We also propose a novel two-level partial order reduction (POR) approach for SNs, which reduces unnecessary interleaving among sensors and among interrupts and tasks within each individual sensor. The POR approach is proved to be sound and complete, preserving LTL-X properties.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ZhengM.pdf2.93 MBAdobe PDF



Page view(s)

checked on Dec 11, 2017


checked on Dec 11, 2017

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.